Home	Quantum Logic Explorer Theorem List (p. 12 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 - 1101-1200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lem4.6.7 1101	Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
0.8  Weakly distributive ortholattices (WDOL)
0.8.1  WDOL law
Axiom	ax-wdol 1102	The WDOL (weakly distributive ortholattice) axiom.
Theorem	wdcom 1103	Any two variables (weakly) commute in a WDOL.
Theorem	wdwom 1104	Prove 2-variable WOML rule in WDOL. This will make all WOML theorems available to us. The proof does not use ax-r3 439 or ax-wom 361. Since this is the same as ax-wom 361, from here on we will freely use those theorems invoking ax-wom 361.
Theorem	wddi1 1105	Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1104.
Theorem	wddi2 1106	The weak distributive law in WDOL.
Theorem	wddi3 1107	The weak distributive law in WDOL.
Theorem	wddi4 1108	The weak distributive law in WDOL.
Theorem	wdid0id5 1109	Show that quantum identity follows from classical identity in a WDOL.
Theorem	wdid0id1 1110	Show a quantum identity that follows from classical identity in a WDOL.
Theorem	wdid0id2 1111	Show a quantum identity that follows from classical identity in a WDOL.
Theorem	wdid0id3 1112	Show a quantum identity that follows from classical identity in a WDOL.
Theorem	wdid0id4 1113	Show a quantum identity that follows from classical identity in a WDOL.
Theorem	wdka4o 1114	Show WDOL analog of WOM law.
Theorem	wddi-0 1115	The weak distributive law in WDOL.
Theorem	wddi-1 1116	The weak distributive law in WDOL.
Theorem	wddi-2 1117	The weak distributive law in WDOL.
Theorem	wddi-3 1118	The weak distributive law in WDOL.
Theorem	wddi-4 1119	The weak distributive law in WDOL.
0.9  Modular ortholattices (MOL)
0.9.1  Modular law
Axiom	ax-ml 1120	The modular law axiom.
Theorem	ml 1121	Modular law in equational form.
Theorem	mldual 1122	Dual of modular law.
Theorem	ml2i 1123	Inference version of modular law.
Theorem	mli 1124	Inference version of modular law.
Theorem	mldual2i 1125	Inference version of dual of modular law.
Theorem	mlduali 1126	Inference version of dual of modular law.
Theorem	ml3le 1127	Form of modular law that swaps two terms.
Theorem	ml3 1128	Form of modular law that swaps two terms.
Theorem	vneulem1 1129	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem2 1130	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem3 1131	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem4 1132	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem5 1133	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem6 1134	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem7 1135	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem8 1136	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem9 1137	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem10 1138	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem11 1139	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem12 1140	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem13 1141	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem14 1142	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem15 1143	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem16 1144	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulem 1145	von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96
Theorem	vneulemexp 1146	Expanded version of vneulem 1145.
Theorem	l42modlem1 1147	Lemma for l42mod 1149..
Theorem	l42modlem2 1148	Lemma for l42mod 1149..
Theorem	l42mod 1149	An equation that fails in OML L42 when converted to a Hilbert space equation.
Theorem	modexp 1150	Expansion by modular law.
0.9.2  Arguesian law
Axiom	ax-arg 1151	The Arguesian law as an axiom.
a0 b0 a1 b1 a2 b2      a0 a1 b0 b1 a0 a2 b0 b2 a1 a2 b1 b2
Theorem	dp15lema 1152	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a1 b1 b2
Theorem	dp15lemb 1153	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a1 b1 a0 b2 a1 b1 b2
Theorem	dp15lemc 1154	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a1 b0 a0 p0 b1 a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
Theorem	dp15lemd 1155	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a2 a0 a1 b1 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2
Theorem	dp15leme 1156	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a2 b0 a0 p0 b2 a1 a2 a0 a1 b1 b1 b2 a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2
Theorem	dp15lemf 1157	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      a0 a2 b0 a0 p0 b2 a1 a2 b1 a0 a1 b1 b2 a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1
Theorem	dp15lemg 1158	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      a1 a2 b1 b2 a0 a2 b0 b2 b1 a0 a1 c0 c1 b1 a0 a1
Theorem	dp15lemh 1159	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	dp15 1160	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (1)=>(5)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      p0 a1 b1 a2 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	dp53lema 1161	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b1 b0 a0 p0 b1 a0 a1 c0 c1
Theorem	dp53lemb 1162	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
Theorem	dp53lemc 1163	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
Theorem	dp53lemd 1164	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
Theorem	dp53leme 1165	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 p0 a0 b0 b1 c2 c0 c1
Theorem	dp53lemf 1166	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      a0 a0 b0 b1 c2 c0 c1
Theorem	dp53lemg 1167	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	dp53 1168	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (5)=>(3)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	dp35lemg 1169	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	dp35lemf 1170	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      a0 a0 b0 b1 c2 c0 c1
Theorem	dp35leme 1171	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 p0 a0 b0 b1 c2 c0 c1
Theorem	dp35lemd 1172	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 p0 b0 a0 b0 b1 c2 c0 c1
Theorem	dp35lemc 1173	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 b0 b1 c2 c0 c1 b0 b1 c2 c0 c1
Theorem	dp35lemb 1174	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 b1 c2 c0 c1 b0 b1 a0 a1 c0 c1
Theorem	dp35lembb 1175	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b0 a0 p0 b0 b1 a0 a1 c0 c1
Theorem	dp35lema 1176	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      b1 b0 a0 p0 b1 a0 a1 c0 c1
Theorem	dp35lem0 1177	Part of proof (3)=>(5) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	dp35 1178	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(5)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      p0 a1 b1 a2 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	dp34 1179	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(4)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2       a0 b1 c2 c0 c1
Theorem	dp41lema 1180	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      a0 b0 a1 b1 a0 b1 c2 c0 c1
Theorem	dp41lemb 1181	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 c2 a0 b0 b1 a0 a1 b1
Theorem	dp41lemc0 1182	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      a0 b0 b1 a0 a1 b1 a0 b1 a0 b0 a1 b1
Theorem	dp41lemc 1183	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 a0 b0 b1 a0 a1 b1 c2 a0 b1 c2 c0 c1
Theorem	dp41lemd 1184	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 a0 b1 c2 c0 c1 c2 c0 c1 c2 a0 b1
Theorem	dp41leme 1185	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 c0 c1 c2 a0 b1 c0 c1 a0 b0 b1 b1 a0 a1
Theorem	dp41lemf 1186	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c0 c1 a0 b0 b1 b1 a0 a1 b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1
Theorem	dp41lemg 1187	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      b1 b2 a1 a2 b1 a0 a1 a0 a2 b0 b2 a0 b0 b1 b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0
Theorem	dp41lemh 1188	Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)".
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      b1 b2 a1 a2 a0 a1 b1 a0 a2 b0 b2 b1 a0 b0 b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2
Theorem	dp41lemj 1189	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      b1 b2 a1 a2 a0 a2 b2 a0 a2 b0 b2 b1 a2 b2 b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2
Theorem	dp41lemk 1190	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      b1 b2 a1 a2 b2 a0 a2 a0 a2 b0 b2 a2 b1 b2 c0 b2 a0 a2 c1 a2 b1 b2
Theorem	dp41leml 1191	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c0 b2 a0 a2 c1 a2 b1 b2 c0 c1
Theorem	dp41lemm 1192	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 c0 c1
Theorem	dp41 1193	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (4)=>(1)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p2 a0 b0 a1 b1      p2 a2 b2      c2 c0 c1
Theorem	dp32 1194	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(2)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2       a0 a1 c2 c0 c1 b0 b1 c2 c0 c1
Theorem	dp23 1195	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (2)=>(3)
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	xdp41 1196	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a0 b0 a1 b1 a2 b2      p2 a0 b0 a1 b1      p2 a2 b2      c2 c0 c1
Theorem	xdp15 1197	Part of proof (1)=>(5) in Day/Pickering 1982.
a2 a0 a1 b1      p0 a1 b1 a2 b2       b0 a0 p0      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1
Theorem	xdp53 1198	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1      p0 a1 b1 a2 b2       a0 b0 a1 b1 a2 b2       a0 b0 b1 c2 c0 c1
Theorem	xxdp41 1199	Part of proof (4)=>(1) in Day/Pickering 1982.
p2 a2 b2      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1      c2 c0 c1
Theorem	xxdp15 1200	Part of proof (1)=>(5) in Day/Pickering 1982.
p2 a2 b2      c0 a1 a2 b1 b2      c1 a0 a2 b0 b2      c2 a0 a1 b0 b1       a2 a0 a1 b1       b0 a0 p0       a0 b0 a1 b1 a2 b2      p0 a1 b1 a2 b2      p2 a0 b0 a1 b1      a0 a1 b0 a0 p0 b1 c0 c1 b1 a0 a1

< 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

---

Copyright terms: Public domain

< Previous  Next >