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

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

0.8  Weakly distributive ortholattices (WDOL)

0.8.1  WDOL law

Axiomax-wdol 1102 The WDOL (weakly distributive ortholattice) axiom.
((ab) ∪ (ab )) = 1

Theoremwdcom 1103 Any two variables (weakly) commute in a WDOL.
C (a, b) = 1

Theoremwdwom 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.
(a ∪ (ab)) = 1       (b ∪ (ab )) = 1

Theoremwddi1 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.
((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1

Theoremwddi2 1106 The weak distributive law in WDOL.
(((ab) ∩ c) ≡ ((ac) ∪ (bc))) = 1

Theoremwddi3 1107 The weak distributive law in WDOL.
((a ∪ (bc)) ≡ ((ab) ∩ (ac))) = 1

Theoremwddi4 1108 The weak distributive law in WDOL.
(((ab) ∪ c) ≡ ((ac) ∩ (bc))) = 1

Theoremwdid0id5 1109 Show that quantum identity follows from classical identity in a WDOL.
(a0 b) = 1       (ab) = 1

Theoremwdid0id1 1110 Show a quantum identity that follows from classical identity in a WDOL.
(a0 b) = 1       (a1 b) = 1

Theoremwdid0id2 1111 Show a quantum identity that follows from classical identity in a WDOL.
(a0 b) = 1       (a2 b) = 1

Theoremwdid0id3 1112 Show a quantum identity that follows from classical identity in a WDOL.
(a0 b) = 1       (a3 b) = 1

Theoremwdid0id4 1113 Show a quantum identity that follows from classical identity in a WDOL.
(a0 b) = 1       (a4 b) = 1

Theoremwdka4o 1114 Show WDOL analog of WOM law.
(a0 b) = 1       ((ac) ≡0 (bc)) = 1

Theoremwddi-0 1115 The weak distributive law in WDOL.
((a ∩ (bc)) ≡0 ((ab) ∪ (ac))) = 1

Theoremwddi-1 1116 The weak distributive law in WDOL.
((a ∩ (bc)) ≡1 ((ab) ∪ (ac))) = 1

Theoremwddi-2 1117 The weak distributive law in WDOL.
((a ∩ (bc)) ≡2 ((ab) ∪ (ac))) = 1

Theoremwddi-3 1118 The weak distributive law in WDOL.
((a ∩ (bc)) ≡3 ((ab) ∪ (ac))) = 1

Theoremwddi-4 1119 The weak distributive law in WDOL.
((a ∩ (bc)) ≡4 ((ab) ∪ (ac))) = 1

0.9  Modular ortholattices (MOL)

0.9.1  Modular law

Axiomax-ml 1120 The modular law axiom.
((ab) ∩ (ac)) ≤ (a ∪ (b ∩ (ac)))

Theoremml 1121 Modular law in equational form.
(a ∪ (b ∩ (ac))) = ((ab) ∩ (ac))

Theoremmldual 1122 Dual of modular law.
(a ∩ (b ∪ (ac))) = ((ab) ∪ (ac))

Theoremml2i 1123 Inference version of modular law.
ca       (c ∪ (ba)) = ((cb) ∩ a)

Theoremmli 1124 Inference version of modular law.
ca       ((ab) ∪ c) = (a ∩ (bc))

Theoremmldual2i 1125 Inference version of dual of modular law.
ac       (c ∩ (ba)) = ((cb) ∪ a)

Theoremmlduali 1126 Inference version of dual of modular law.
ac       ((ab) ∩ c) = (a ∪ (bc))

Theoremml3le 1127 Form of modular law that swaps two terms.
(a ∪ (b ∩ (ca))) ≤ (a ∪ (c ∩ (ba)))

Theoremml3 1128 Form of modular law that swaps two terms.
(a ∪ (b ∩ (ca))) = (a ∪ (c ∩ (ba)))

Theoremvneulem1 1129 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((xy) ∪ u) ∩ w) = (((xy) ∪ u) ∩ ((uw) ∩ w))

Theoremvneulem2 1130 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((xy) ∪ u) ∩ ((uw) ∩ w)) = ((((xy) ∩ (uw)) ∪ u) ∩ w)

Theoremvneulem3 1131 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((xy) ∩ (uw)) = 0       ((((xy) ∩ (uw)) ∪ u) ∩ w) = (uw)

Theoremvneulem4 1132 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((xy) ∩ (uw)) = 0       (((xy) ∪ u) ∩ w) = (uw)

Theoremvneulem5 1133 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((xy) ∪ u) ∩ ((xy) ∪ w)) = ((xy) ∪ (((xy) ∪ u) ∩ w))

Theoremvneulem6 1134 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((bc) ∪ d)) = ((ca) ∪ (bd))

Theoremvneulem7 1135 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       ((ca) ∪ (bd)) = (bd)

Theoremvneulem8 1136 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((bc) ∪ d)) = (bd)

Theoremvneulem9 1137 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((ab) ∪ d) ∩ ((ab) ∪ c)) = ((cd) ∪ (ab))

Theoremvneulem10 1138 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((ab) ∪ c) ∩ ((ac) ∪ d)) = (ac)

Theoremvneulem11 1139 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((bc) ∪ d) ∩ ((ac) ∪ d)) = ((cd) ∪ (ab))

Theoremvneulem12 1140 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((cd) ∪ (ab)) ∩ ((cd) ∪ (ab))) = ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab))))

Theoremvneulem13 1141 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab)))) = ((cd) ∪ (ab))

Theoremvneulem14 1142 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       (((cd) ∪ (ab)) ∩ ((cd) ∪ (ab))) = ((cd) ∪ (ab))

Theoremvneulem15 1143 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((((ab) ∪ c) ∩ ((ac) ∪ d)) ∩ (((ab) ∪ d) ∩ ((bc) ∪ d)))

Theoremvneulem16 1144 Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       ((((ab) ∪ c) ∩ ((ac) ∪ d)) ∩ (((ab) ∪ d) ∩ ((bc) ∪ d))) = ((ab) ∪ (cd))

Theoremvneulem 1145 von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Theoremvneulemexp 1146 Expanded version of vneulem 1145.
((ab) ∩ (cd)) = 0       ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Theoreml42modlem1 1147 Lemma for l42mod 1149..
(((ab) ∪ d) ∩ ((ab) ∪ e)) = ((ab) ∪ ((ad) ∩ (be)))

Theoreml42modlem2 1148 Lemma for l42mod 1149..
((((ab) ∩ c) ∪ d) ∩ e) ≤ (((ab) ∪ d) ∩ ((ab) ∪ e))

Theoreml42mod 1149 An equation that fails in OML L42 when converted to a Hilbert space equation.
((((ab) ∩ c) ∪ d) ∩ e) ≤ ((ab) ∪ ((ad) ∩ (be)))

Theoremmodexp 1150 Expansion by modular law.
(a ∩ (bc)) = (a ∩ (b ∪ (c ∩ (ab))))

0.9.2  Arguesian law

Axiomax-arg 1151 The Arguesian law as an axiom.
((a0b0) ∩ (a1b1)) ≤ (a2b2)       ((a0a1) ∩ (b0b1)) ≤ (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))

Theoremdp15lema 1152 Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       ((a0e) ∩ (a1b1)) ≤ (db2)

Theoremdp15lemb 1153 Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))       ((a0a1) ∩ (eb1)) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))

Theoremdp15lemc 1154 Part of proof (1)=>(5) in Day/Pickering 1982.
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 1155 Part of proof (1)=>(5) in Day/Pickering 1982.
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 1156 Part of proof (1)=>(5) in Day/Pickering 1982.
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 1157 Part of proof (1)=>(5) in Day/Pickering 1982.
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 1158 Part of proof (1)=>(5) in Day/Pickering 1982.
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 1159 Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp15 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp53lema 1161 Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))

Theoremdp53lemb 1162 Part of proof (5)=>(3) in Day/Pickering 1982.
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 1163 Part of proof (5)=>(3) in Day/Pickering 1982.
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 1164 Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))

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

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

Theoremdp53lemg 1167 Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp53 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemg 1169 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemf 1170 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35leme 1171 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp35lemd 1172 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))

Theoremdp35lemc 1173 Part of proof (3)=>(5) in Day/Pickering 1982.
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 1174 Part of proof (3)=>(5) in Day/Pickering 1982.
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 1175 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (a0p0)) ≤ (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))

Theoremdp35lema 1176 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))

Theoremdp35lem0 1177 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp35 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremdp34 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))

Theoremdp41lema 1180 Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       ((a0b0) ∩ (a1b1)) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))

Theoremdp41lemb 1181 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1182 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1183 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1184 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1185 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1186 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1187 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1188 Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)".
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 1189 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1190 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1191 Part of proof (4)=>(1) in Day/Pickering 1982.
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 1192 Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremdp41 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremdp32 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ ((a0 ∩ (a1 ∪ (c2 ∩ (c0c1)))) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremdp23 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 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremxdp41 1196 Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))    &   p2 ≤ (a2b2)       c2 ≤ (c0c1)

Theoremxdp15 1197 Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 ∪ (a0 ∩ (a1b1)))    &   p0 = ((a1b1) ∩ (a2b2))    &   e = (b0 ∩ (a0p0))    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremxdp53 1198 Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremxxdp41 1199 Part of proof (4)=>(1) in Day/Pickering 1982.
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       c2 ≤ (c0c1)

Theoremxxdp15 1200 Part of proof (1)=>(5) in Day/Pickering 1982.
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

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 >