P. 2 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 101-200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dff 101	Alternate definition 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
0.1.3  Relationship analogues (ordering; commutation)
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
0.1.4  Commutator (ortholattice theorems)
Theorem	cmtrcom 190	Commutative law for commutator. (Contributed by NM, 24-Jan-1999.)
C (a, b) = C (b, a)
0.1.5  Weak "orthomodular law" in ortholattices. 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