Theorem List for Quantum Logic Explorer - 1101-1200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremlem4.6.6i4j2 1101 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 2. (Contributed by Roy F. Longton, 2-Jul-2005.)
((a4 b) ∪ (a2 b)) = (a0 b)

Theoremcom3iia 1102 The dual of com3ii 457. (Contributed by Roy F. Longton, 2-Jul-2005.)
a C b       (a ∪ (ab)) = (ab)

Theoremlem4.6.7 1103 Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-2005.)
ab       b ≤ (a1 b)

0.8  Weakly distributive ortholattices (WDOL)

0.8.1  WDOL law

Axiomax-wdol 1104 The WDOL (weakly distributive ortholattice) axiom. (Contributed by NM, 4-Mar-2006.)
((ab) ∪ (ab )) = 1

Theoremwdcom 1105 Any two variables (weakly) commute in a WDOL. (Contributed by NM, 4-Mar-2006.)
C (a, b) = 1

Theoremwdwom 1106 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. (Contributed by NM, 4-Mar-2006.)
(a ∪ (ab)) = 1       (b ∪ (ab )) = 1

Theoremwddi1 1107 Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1106. (Contributed by NM, 4-Mar-2006.)
((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1

Theoremwddi2 1108 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
(((ab) ∩ c) ≡ ((ac) ∪ (bc))) = 1

Theoremwddi3 1109 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 1

Theoremwddi4 1110 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
(((ab) ∪ c) ≡ ((ac) ∩ (bc))) = 1

Theoremwdid0id5 1111 Show that quantum identity follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       (ab) = 1

Theoremwdid0id1 1112 Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       (a1 b) = 1

Theoremwdid0id2 1113 Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       (a2 b) = 1

Theoremwdid0id3 1114 Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       (a3 b) = 1

Theoremwdid0id4 1115 Show a quantum identity that follows from classical identity in a WDOL. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       (a4 b) = 1

Theoremwdka4o 1116 Show WDOL analog of WOM law. (Contributed by NM, 5-Mar-2006.)
(a0 b) = 1       ((ac) ≡0 (bc)) = 1

Theoremwddi-0 1117 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (bc)) ≡0 ((ab) ∪ (ac))) = 1

Theoremwddi-1 1118 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (bc)) ≡1 ((ab) ∪ (ac))) = 1

Theoremwddi-2 1119 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (bc)) ≡2 ((ab) ∪ (ac))) = 1

Theoremwddi-3 1120 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (bc)) ≡3 ((ab) ∪ (ac))) = 1

Theoremwddi-4 1121 The weak distributive law in WDOL. (Contributed by NM, 5-Mar-2006.)
((a ∩ (bc)) ≡4 ((ab) ∪ (ac))) = 1

0.9  Modular ortholattices (MOL)

0.9.1  Modular law

Axiomax-ml 1122 The modular law axiom. (Contributed by NM, 15-Mar-2010.)
((ab) ∩ (ac)) ≤ (a ∪ (b ∩ (ac)))

Theoremml 1123 Modular law in equational form. (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(a ∪ (b ∩ (ac))) = ((ab) ∩ (ac))

Theoremmldual 1124 Dual of modular law. (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(a ∩ (b ∪ (ac))) = ((ab) ∪ (ac))

Theoremml2i 1125 Inference version of modular law. (Contributed by NM, 1-Apr-2012.)
ca       (c ∪ (ba)) = ((cb) ∩ a)

Theoremmli 1126 Inference version of modular law. (Contributed by NM, 1-Apr-2012.)
ca       ((ab) ∪ c) = (a ∩ (bc))

Theoremmldual2i 1127 Inference version of dual of modular law. (Contributed by NM, 1-Apr-2012.)
ac       (c ∩ (ba)) = ((cb) ∪ a)

Theoremmlduali 1128 Inference version of dual of modular law. (Contributed by NM, 1-Apr-2012.)
ac       ((ab) ∩ c) = (a ∪ (bc))

Theoremml3le 1129 Form of modular law that swaps two terms. (Contributed by NM, 1-Apr-2012.)
(a ∪ (b ∩ (ca))) ≤ (a ∪ (c ∩ (ba)))

Theoremml3 1130 Form of modular law that swaps two terms. (Contributed by NM, 1-Apr-2012.)
(a ∪ (b ∩ (ca))) = (a ∪ (c ∩ (ba)))

Theoremvneulem1 1131 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((xy) ∪ u) ∩ w) = (((xy) ∪ u) ∩ ((uw) ∩ w))

Theoremvneulem2 1132 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((xy) ∪ u) ∩ ((uw) ∩ w)) = ((((xy) ∩ (uw)) ∪ u) ∩ w)

Theoremvneulem3 1133 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((xy) ∩ (uw)) = 0       ((((xy) ∩ (uw)) ∪ u) ∩ w) = (uw)

Theoremvneulem4 1134 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((xy) ∩ (uw)) = 0       (((xy) ∪ u) ∩ w) = (uw)

Theoremvneulem5 1135 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
(((xy) ∪ u) ∩ ((xy) ∪ w)) = ((xy) ∪ (((xy) ∪ u) ∩ w))

Theoremvneulem6 1136 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((bc) ∪ d)) = ((ca) ∪ (bd))

Theoremvneulem7 1137 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((ca) ∪ (bd)) = (bd)

Theoremvneulem8 1138 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((bc) ∪ d)) = (bd)

Theoremvneulem9 1139 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((ab) ∪ c)) = ((cd) ∪ (ab))

Theoremvneulem10 1140 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((ab) ∪ c) ∩ ((ac) ∪ d)) = (ac)

Theoremvneulem11 1141 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((bc) ∪ d) ∩ ((ac) ∪ d)) = ((cd) ∪ (ab))

Theoremvneulem12 1142 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
(((cd) ∪ (ab)) ∩ ((cd) ∪ (ab))) = ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab))))

Theoremvneulem13 1143 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab)))) = ((cd) ∪ (ab))

Theoremvneulem14 1144 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       (((cd) ∪ (ab)) ∩ ((cd) ∪ (ab))) = ((cd) ∪ (ab))

Theoremvneulem15 1145 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((((ab) ∪ c) ∩ ((ac) ∪ d)) ∩ (((ab) ∪ d) ∩ ((bc) ∪ d)))

Theoremvneulem16 1146 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((((ab) ∪ c) ∩ ((ac) ∪ d)) ∩ (((ab) ∪ d) ∩ ((bc) ∪ d))) = ((ab) ∪ (cd))

Theoremvneulem 1147 von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Theoremvneulemexp 1148 Expanded version of vneulem 1147. (Contributed by NM, 31-Mar-2011.)
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Theoreml42modlem1 1149 Lemma for l42mod 1151.. (Contributed by NM, 8-Apr-2012.)
(((ab) ∪ d) ∩ ((ab) ∪ e)) = ((ab) ∪ ((ad) ∩ (be)))

Theoreml42modlem2 1150 Lemma for l42mod 1151.. (Contributed by NM, 8-Apr-2012.)
((((ab) ∩ c) ∪ d) ∩ e) ≤ (((ab) ∪ d) ∩ ((ab) ∪ e))

Theoreml42mod 1151 An equation that fails in OML L42 when converted to a Hilbert space equation. (Contributed by NM, 8-Apr-2012.)
((((ab) ∩ c) ∪ d) ∩ e) ≤ ((ab) ∪ ((ad) ∩ (be)))

Theoremmodexp 1152 Expansion by modular law. (Contributed by NM, 10-Apr-2012.)
(a ∩ (bc)) = (a ∩ (b ∪ (c ∩ (ab))))

0.9.2  Arguesian law

Axiomax-arg 1153 The Arguesian law as an axiom. (Contributed by NM, 1-Apr-2012.)
((a0b0) ∩ (a1b1)) ≤ (a2b2)       ((a0a1) ∩ (b0b1)) ≤ (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))

Theoremdp15lema 1154 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       ((a0e) ∩ (a1b1)) ≤ (db2)

Theoremdp15lemb 1155 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       ((a0a1) ∩ (eb1)) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))

Theoremdp15lemc 1156 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 10-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)))

Theoremdp15lemd 1157 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))) = (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)))

Theoremdp15leme 1158 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2))) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)))

Theoremdp15lemf 1159 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))) ≤ (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))

Theoremdp15lemg 1160 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 1-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))       (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp15lemh 1161 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp15 1162 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) (Contributed by NM, 1-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp53lema 1163 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))

Theoremdp53lemb 1164 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))

Theoremdp53lemc 1165 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))

Theoremdp53lemd 1166 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))

Theoremdp53leme 1167 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp53lemf 1168 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp53lemg 1169 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp53 1170 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) (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemg 1171 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemf 1172 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35leme 1173 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemd 1174 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))

Theoremdp35lemc 1175 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))

Theoremdp35lemb 1176 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 2-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))

Theoremdp35lembb 1177 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))

Theoremdp35lema 1178 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))

Theoremdp35lem0 1179 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp35 1180 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) (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp34 1181 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) (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))

Theoremdp41lema 1182 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       ((a0b0) ∩ (a1b1)) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))

Theoremdp41lemb 1183 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 = ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1))

Theoremdp41lemc0 1184 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 4-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) = ((a0b1) ∪ ((a0b0) ∩ (a1b1)))

Theoremdp41lemc 1185 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1)) ≤ (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1))))

Theoremdp41lemd 1186 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1)))) = (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1))))

Theoremdp41leme 1187 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1)))) ≤ ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))

Theoremdp41lemf 1188 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))) = (((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1)))))

Theoremdp41lemg 1189 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1))))) = (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0)))))

Theoremdp41lemh 1190 Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)". (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0))))) ≤ (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2)))))

Theoremdp41lemj 1191 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2))))) = (((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2)))))

Theoremdp41lemk 1192 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       (((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2))))) = ((c0 ∪ (b2 ∩ (a0a2))) ∪ (c1 ∪ (a2 ∩ (b1b2))))

Theoremdp41leml 1193 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       ((c0 ∪ (b2 ∩ (a0a2))) ∪ (c1 ∪ (a2 ∩ (b1b2)))) = (c0c1)

Theoremdp41lemm 1194 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremdp41 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). (4)=>(1) (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremdp32 1196 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) (Contributed by NM, 4-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ ((a0 ∩ (a1 ∪ (c2 ∩ (c0c1)))) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp23 1197 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) (Contributed by NM, 4-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremxdp41 1198 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremxdp15 1199 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremxdp53 1200 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

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-1217
 Copyright terms: Public domain < Previous  Next >