P. 2 of Theorem List - Quantum Logic Explorer

Home	Quantum Logic Explorer Theorem List (p. 2 of 13)	< Previous Next >
		Browser slow? Try the Unicode 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".


Theorem	or0 102	Disjunction with 0.


Theorem	or0r 103	Disjunction with 0.


Theorem	or1 104	Disjunction with 1.


Theorem	or1r 105	Disjunction with 1.


Theorem	an1 106	Conjunction with 1.


Theorem	an1r 107	Conjunction with 1.


Theorem	an0 108	Conjunction with 0.


Theorem	an0r 109	Conjunction with 0.


Theorem	oridm 110	Idempotent law.


Theorem	anidm 111	Idempotent law.


Theorem	orordi 112	Distribution of disjunction over disjunction.


Theorem	orordir 113	Distribution of disjunction over disjunction.


Theorem	anandi 114	Distribution of conjunction over conjunction.


Theorem	anandir 115	Distribution of conjunction over conjunction.


Theorem	biid 116	Identity law.


Theorem	1b 117	Identity law.


Theorem	bi1 118	Identity inference.


Theorem	1bi 119	Identity inference.


Theorem	orabs 120	Absorption law.


Theorem	anabs 121	Absorption law.


Theorem	conb 122	Contraposition law.


Theorem	leoa 123	Relation between two methods of expressing "less than or equal to".


Theorem	leao 124	Relation between two methods of expressing "less than or equal to".


Theorem	mi 125	Mittelstaedt implication.


Theorem	di 126	Dishkant implication.


Theorem	omlem1 127	Lemma in proof of Th. 1 of Pavicic 1987.


Theorem	omlem2 128	Lemma in proof of Th. 1 of Pavicic 1987.


0.1.3 Relationship analogues (ordering; commutation)

Definition	df-le 129	Define 'less than or equal to' analogue.


Definition	df-le1 130	Define 'less than or equal to'. See df-le2 131 for the other direction.


Definition	df-le2 131	Define 'less than or equal to'. See df-le1 130 for the other direction.


Definition	df-c1 132	Define 'commutes'. See df-c2 133 for the other direction.


Definition	df-c2 133	Define 'commutes'. See df-c1 132 for the other direction.


Definition	df-cmtr 134	Define 'commutator'.


Theorem	df2le1 135	Alternate definition of 'less than or equal to'.


Theorem	df2le2 136	Alternate definition of 'less than or equal to'.


Theorem	letr 137	Transitive law for l.e.


Theorem	bltr 138	Transitive inference.


Theorem	lbtr 139	Transitive inference.


Theorem	le3tr1 140	Transitive inference useful for introducing definitions.


Theorem	le3tr2 141	Transitive inference useful for eliminating definitions.


Theorem	bile 142	Biconditional to l.e.


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).


Theorem	qlhoml1b 144	An ortholattice inequality, corresponding to a theorem provable in Hilbert space.


Theorem	lebi 145	L.e. to biconditional.


Theorem	le1 146	Anything is l.e. 1.


Theorem	le0 147	0 is l.e. anything.


Theorem	leid 148	Identity law for less-than-or-equal.


Theorem	ler 149	Add disjunct to right of l.e.


Theorem	lerr 150	Add disjunct to right of l.e.


Theorem	lel 151	Add conjunct to left of l.e.


Theorem	leror 152	Add disjunct to right of both sides.


Theorem	leran 153	Add conjunct to right of both sides.


Theorem	lecon 154	Contrapositive for l.e.


Theorem	lecon1 155	Contrapositive for l.e.


Theorem	lecon2 156	Contrapositive for l.e.


Theorem	lecon3 157	Contrapositive for l.e.


Theorem	leo 158	L.e. absorption.


Theorem	leor 159	L.e. absorption.


Theorem	lea 160	L.e. absorption.


Theorem	lear 161	L.e. absorption.


Theorem	leao1 162	L.e. absorption.


Theorem	leao2 163	L.e. absorption.


Theorem	leao3 164	L.e. absorption.


Theorem	leao4 165	L.e. absorption.


Theorem	lelor 166	Add disjunct to left of both sides.


Theorem	lelan 167	Add conjunct to left of both sides.


Theorem	le2or 168	Disjunction of 2 l.e.'s.


Theorem	le2an 169	Conjunction of 2 l.e.'s.


Theorem	lel2or 170	Disjunction of 2 l.e.'s.


Theorem	lel2an 171	Conjunction of 2 l.e.'s.


Theorem	ler2or 172	Disjunction of 2 l.e.'s.


Theorem	ler2an 173	Conjunction of 2 l.e.'s.


Theorem	ledi 174	Half of distributive law.


Theorem	ledir 175	Half of distributive law.


Theorem	ledio 176	Half of distributive law.


Theorem	ledior 177	Half of distributive law.


Theorem	comm0 178	Commutation with 0. Kalmbach 83 p. 20.


Theorem	comm1 179	Commutation with 1. Kalmbach 83 p. 20.


Theorem	lecom 180	Comparable elements commute. Beran 84 2.3(iii) p. 40.


Theorem	bctr 181	Transitive inference.


Theorem	cbtr 182	Transitive inference.


Theorem	comcom2 183	Commutation equivalence. Kalmbach 83 p. 23. Does not use OML.


Theorem	comorr 184	Commutation law. Does not use OML.


Theorem	coman1 185	Commutation law. Does not use OML.


Theorem	coman2 186	Commutation law. Does not use OML.


Theorem	comid 187	Identity law for commutation. Does not use OML.


Theorem	distlem 188	Distributive law inference (uses OL only).


Theorem	str 189	Strengthening rule.


0.1.4 Commutator (ortholattice theorems)

Theorem	cmtrcom 190	Commutative law for commutator.


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.


Theorem	wa2 192	Weak A2.


Theorem	wa3 193	Weak A3.


Theorem	wa4 194	Weak A4.


Theorem	wa5 195	Weak A5.


Theorem	wa6 196	Weak A6.


Theorem	wr1 197	Weak R1.


Theorem	wr3 198	Weak R3.


Theorem	wr4 199	Weak R4.


Theorem	wa5b 200	Absorption law.

< 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 >