P. 2 of Theorem List - Quantum Logic Explorer

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

**Theorem List for Quantum Logic Explorer -** 101-200 *Has distinct variable group(s)
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

0.1.3 Relationship analogues (ordering; commutation)

Definition	df-le 129	Define 'less than or equal to' analogue.
(a ≤₂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

0.1.4 Commutator (ortholattice theorems)

Theorem	cmtrcom 190	Commutative law for commutator.
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.
(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 >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1215

< Previous Next >