Home | Quantum
Logic Explorer Theorem List (p. 2 of 13) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > QLE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dff 101 | Alternate defintion of "false". |
0 = (a ∩ a⊥ ) | ||
Theorem | or0 102 | Disjunction with 0. |
(a ∪ 0) = a | ||
Theorem | or0r 103 | Disjunction with 0. |
(0 ∪ a) = a | ||
Theorem | or1 104 | Disjunction with 1. |
(a ∪ 1) = 1 | ||
Theorem | or1r 105 | Disjunction with 1. |
(1 ∪ a) = 1 | ||
Theorem | an1 106 | Conjunction with 1. |
(a ∩ 1) = a | ||
Theorem | an1r 107 | Conjunction with 1. |
(1 ∩ a) = a | ||
Theorem | an0 108 | Conjunction with 0. |
(a ∩ 0) = 0 | ||
Theorem | an0r 109 | Conjunction with 0. |
(0 ∩ a) = 0 | ||
Theorem | oridm 110 | Idempotent law. |
(a ∪ a) = a | ||
Theorem | anidm 111 | Idempotent law. |
(a ∩ a) = a | ||
Theorem | orordi 112 | Distribution of disjunction over disjunction. |
(a ∪ (b ∪ c)) = ((a ∪ b) ∪ (a ∪ c)) | ||
Theorem | orordir 113 | Distribution of disjunction over disjunction. |
((a ∪ b) ∪ c) = ((a ∪ c) ∪ (b ∪ c)) | ||
Theorem | anandi 114 | Distribution of conjunction over conjunction. |
(a ∩ (b ∩ c)) = ((a ∩ b) ∩ (a ∩ c)) | ||
Theorem | anandir 115 | Distribution of conjunction over conjunction. |
((a ∩ b) ∩ c) = ((a ∩ c) ∩ (b ∩ c)) | ||
Theorem | biid 116 | Identity law. |
(a ≡ a) = 1 | ||
Theorem | 1b 117 | Identity law. |
(1 ≡ a) = a | ||
Theorem | bi1 118 | Identity inference. |
a = b ⇒ (a ≡ b) = 1 | ||
Theorem | 1bi 119 | Identity inference. |
a = b ⇒ 1 = (a ≡ b) | ||
Theorem | orabs 120 | Absorption law. |
(a ∪ (a ∩ b)) = a | ||
Theorem | anabs 121 | Absorption law. |
(a ∩ (a ∪ b)) = a | ||
Theorem | conb 122 | Contraposition law. |
(a ≡ b) = (a⊥ ≡ b⊥ ) | ||
Theorem | leoa 123 | Relation between two methods of expressing "less than or equal to". |
(a ∪ c) = b ⇒ (a ∩ b) = a | ||
Theorem | leao 124 | Relation between two methods of expressing "less than or equal to". |
(c ∩ b) = a ⇒ (a ∪ b) = b | ||
Theorem | mi 125 | Mittelstaedt implication. |
((a ∪ b) ≡ b) = (b ∪ (a⊥ ∩ b⊥ )) | ||
Theorem | di 126 | Dishkant implication. |
((a ∩ b) ≡ a) = (a⊥ ∪ (a ∩ b)) | ||
Theorem | omlem1 127 | Lemma in proof of Th. 1 of Pavicic 1987. |
((a ∪ (a⊥ ∩ (a ∪ b))) ∪ (a ∪ b)) = (a ∪ b) | ||
Theorem | omlem2 128 | Lemma in proof of Th. 1 of Pavicic 1987. |
((a ∪ b)⊥ ∪ (a ∪ (a⊥ ∩ (a ∪ b)))) = 1 | ||
Definition | df-le 129 | Define 'less than or equal to' analogue. |
(a ≤2 b) = ((a ∪ b) ≡ b) | ||
Definition | df-le1 130 | Define 'less than or equal to'. See df-le2 131 for the other direction. |
(a ∪ b) = b ⇒ a ≤ b | ||
Definition | df-le2 131 | Define 'less than or equal to'. See df-le1 130 for the other direction. |
a ≤ b ⇒ (a ∪ b) = b | ||
Definition | df-c1 132 | Define 'commutes'. See df-c2 133 for the other direction. |
a = ((a ∩ b) ∪ (a ∩ b⊥ )) ⇒ a C b | ||
Definition | df-c2 133 | Define 'commutes'. See df-c1 132 for the other direction. |
a C b ⇒ a = ((a ∩ b) ∪ (a ∩ b⊥ )) | ||
Definition | df-cmtr 134 | Define 'commutator'. |
C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) | ||
Theorem | df2le1 135 | Alternate definition of 'less than or equal to'. |
(a ∩ b) = a ⇒ a ≤ b | ||
Theorem | df2le2 136 | Alternate definition of 'less than or equal to'. |
a ≤ b ⇒ (a ∩ b) = a | ||
Theorem | letr 137 | Transitive law for l.e. |
a ≤ b & b ≤ c ⇒ a ≤ c | ||
Theorem | bltr 138 | Transitive inference. |
a = b & b ≤ c ⇒ a ≤ c | ||
Theorem | lbtr 139 | Transitive inference. |
a ≤ b & b = c ⇒ a ≤ c | ||
Theorem | le3tr1 140 | Transitive inference useful for introducing definitions. |
a ≤ b & c = a & d = b ⇒ c ≤ d | ||
Theorem | le3tr2 141 | Transitive inference useful for eliminating definitions. |
a ≤ b & a = c & b = d ⇒ c ≤ d | ||
Theorem | bile 142 | Biconditional to l.e. |
a = b ⇒ a ≤ b | ||
Theorem | qlhoml1a 143 | An ortholattice inequality, corresponding to a theorem provable in Hilbert space. Part of Definition 2.1 p. 2092, in M. Pavicic and N. Megill, "Quantum and Classical Implicational Algebras with Primitive Implication," _Int. J. of Theor. Phys._ 37, 2091-2098 (1998). |
a ≤ a⊥ ⊥ | ||
Theorem | qlhoml1b 144 | An ortholattice inequality, corresponding to a theorem provable in Hilbert space. |
a⊥ ⊥ ≤ a | ||
Theorem | lebi 145 | L.e. to biconditional. |
a ≤ b & b ≤ a ⇒ a = b | ||
Theorem | le1 146 | Anything is l.e. 1. |
a ≤ 1 | ||
Theorem | le0 147 | 0 is l.e. anything. |
0 ≤ a | ||
Theorem | leid 148 | Identity law for less-than-or-equal. |
a ≤ a | ||
Theorem | ler 149 | Add disjunct to right of l.e. |
a ≤ b ⇒ a ≤ (b ∪ c) | ||
Theorem | lerr 150 | Add disjunct to right of l.e. |
a ≤ b ⇒ a ≤ (c ∪ b) | ||
Theorem | lel 151 | Add conjunct to left of l.e. |
a ≤ b ⇒ (a ∩ c) ≤ b | ||
Theorem | leror 152 | Add disjunct to right of both sides. |
a ≤ b ⇒ (a ∪ c) ≤ (b ∪ c) | ||
Theorem | leran 153 | Add conjunct to right of both sides. |
a ≤ b ⇒ (a ∩ c) ≤ (b ∩ c) | ||
Theorem | lecon 154 | Contrapositive for l.e. |
a ≤ b ⇒ b⊥ ≤ a⊥ | ||
Theorem | lecon1 155 | Contrapositive for l.e. |
a⊥ ≤ b⊥ ⇒ b ≤ a | ||
Theorem | lecon2 156 | Contrapositive for l.e. |
a⊥ ≤ b ⇒ b⊥ ≤ a | ||
Theorem | lecon3 157 | Contrapositive for l.e. |
a ≤ b⊥ ⇒ b ≤ a⊥ | ||
Theorem | leo 158 | L.e. absorption. |
a ≤ (a ∪ b) | ||
Theorem | leor 159 | L.e. absorption. |
a ≤ (b ∪ a) | ||
Theorem | lea 160 | L.e. absorption. |
(a ∩ b) ≤ a | ||
Theorem | lear 161 | L.e. absorption. |
(a ∩ b) ≤ b | ||
Theorem | leao1 162 | L.e. absorption. |
(a ∩ b) ≤ (a ∪ c) | ||
Theorem | leao2 163 | L.e. absorption. |
(b ∩ a) ≤ (a ∪ c) | ||
Theorem | leao3 164 | L.e. absorption. |
(a ∩ b) ≤ (c ∪ a) | ||
Theorem | leao4 165 | L.e. absorption. |
(b ∩ a) ≤ (c ∪ a) | ||
Theorem | lelor 166 | Add disjunct to left of both sides. |
a ≤ b ⇒ (c ∪ a) ≤ (c ∪ b) | ||
Theorem | lelan 167 | Add conjunct to left of both sides. |
a ≤ b ⇒ (c ∩ a) ≤ (c ∩ b) | ||
Theorem | le2or 168 | Disjunction of 2 l.e.'s. |
a ≤ b & c ≤ d ⇒ (a ∪ c) ≤ (b ∪ d) | ||
Theorem | le2an 169 | Conjunction of 2 l.e.'s. |
a ≤ b & c ≤ d ⇒ (a ∩ c) ≤ (b ∩ d) | ||
Theorem | lel2or 170 | Disjunction of 2 l.e.'s. |
a ≤ b & c ≤ b ⇒ (a ∪ c) ≤ b | ||
Theorem | lel2an 171 | Conjunction of 2 l.e.'s. |
a ≤ b & c ≤ b ⇒ (a ∩ c) ≤ b | ||
Theorem | ler2or 172 | Disjunction of 2 l.e.'s. |
a ≤ b & a ≤ c ⇒ a ≤ (b ∪ c) | ||
Theorem | ler2an 173 | Conjunction of 2 l.e.'s. |
a ≤ b & a ≤ c ⇒ a ≤ (b ∩ c) | ||
Theorem | ledi 174 | Half of distributive law. |
((a ∩ b) ∪ (a ∩ c)) ≤ (a ∩ (b ∪ c)) | ||
Theorem | ledir 175 | Half of distributive law. |
((b ∩ a) ∪ (c ∩ a)) ≤ ((b ∪ c) ∩ a) | ||
Theorem | ledio 176 | Half of distributive law. |
(a ∪ (b ∩ c)) ≤ ((a ∪ b) ∩ (a ∪ c)) | ||
Theorem | ledior 177 | Half of distributive law. |
((b ∩ c) ∪ a) ≤ ((b ∪ a) ∩ (c ∪ a)) | ||
Theorem | comm0 178 | Commutation with 0. Kalmbach 83 p. 20. |
a C 0 | ||
Theorem | comm1 179 | Commutation with 1. Kalmbach 83 p. 20. |
1 C a | ||
Theorem | lecom 180 | Comparable elements commute. Beran 84 2.3(iii) p. 40. |
a ≤ b ⇒ a C b | ||
Theorem | bctr 181 | Transitive inference. |
a = b & b C c ⇒ a C c | ||
Theorem | cbtr 182 | Transitive inference. |
a C b & b = c ⇒ a C c | ||
Theorem | comcom2 183 | Commutation equivalence. Kalmbach 83 p. 23. Does not use OML. |
a C b ⇒ a C b⊥ | ||
Theorem | comorr 184 | Commutation law. Does not use OML. |
a C (a ∪ b) | ||
Theorem | coman1 185 | Commutation law. Does not use OML. |
(a ∩ b) C a | ||
Theorem | coman2 186 | Commutation law. Does not use OML. |
(a ∩ b) C b | ||
Theorem | comid 187 | Identity law for commutation. Does not use OML. |
a C a | ||
Theorem | distlem 188 | Distributive law inference (uses OL only). |
(a ∩ (b ∪ c)) ≤ b ⇒ (a ∩ (b ∪ c)) = ((a ∩ b) ∪ (a ∩ c)) | ||
Theorem | str 189 | Strengthening rule. |
a ≤ (b ∪ c) & (a ∩ (b ∪ c)) ≤ b ⇒ a ≤ b | ||
Theorem | cmtrcom 190 | Commutative law for commutator. |
C (a, b) = C (b, a) | ||
All theorems here do not require R3 and are true in all ortholattices. | ||
Theorem | wa1 191 | Weak A1. |
(a ≡ a⊥ ⊥ ) = 1 | ||
Theorem | wa2 192 | Weak A2. |
((a ∪ b) ≡ (b ∪ a)) = 1 | ||
Theorem | wa3 193 | Weak A3. |
(((a ∪ b) ∪ c) ≡ (a ∪ (b ∪ c))) = 1 | ||
Theorem | wa4 194 | Weak A4. |
((a ∪ (b ∪ b⊥ )) ≡ (b ∪ b⊥ )) = 1 | ||
Theorem | wa5 195 | Weak A5. |
((a ∪ (a⊥ ∪ b⊥ )⊥ ) ≡ a) = 1 | ||
Theorem | wa6 196 | Weak A6. |
((a ≡ b) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )) = 1 | ||
Theorem | wr1 197 | Weak R1. |
(a ≡ b) = 1 ⇒ (b ≡ a) = 1 | ||
Theorem | wr3 198 | Weak R3. |
(1 ≡ a) = 1 ⇒ a = 1 | ||
Theorem | wr4 199 | Weak R4. |
(a ≡ b) = 1 ⇒ (a⊥ ≡ b⊥ ) = 1 | ||
Theorem | wa5b 200 | Absorption law. |
((a ∪ (a ∩ b)) ≡ a) = 1 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |