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