[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 13 of 13)
< Previous  Wrap >
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 - 1201-1217   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremxxdp41 1201 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
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 1202 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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)))
 
Theoremxxdp53 1203 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theoremxdp45lem 1204 Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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)))
 
Theoremxdp43lem 1205 Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theoremxdp45 1206 Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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)))
 
Theoremxdp43 1207 Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
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))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theorem3dp43 1208 "3OA" version of xdp43 1207. Changed a2 to a1 and b2 to b1. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1a1) ∩ (b1b1))    &   c1 = ((a0a1) ∩ (b0b1))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a1 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a1b1))    &   p0 = ((a1b1) ∩ (a1b1))    &   p2 = ((a0b0) ∩ (a1b1))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theoremoadp35lemg 1209 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theoremoadp35lemf 1210 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
 
Theoremoadp35lemc 1211 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
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))))
 
Theoremoadp35 1212 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)))
 
Theoremtestmod 1213 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a)
 
Theoremtestmod1 1214 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
 
Theoremtestmod2 1215 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
 
Theoremtestmod2expanded 1216 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))
 
Theoremtestmod3 1217 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (((ca) ∪ ((bc) ∩ (da))) ∩ (b ∩ (d ∪ ((ac) ∩ (bd))))))
    < Previous  Wrap >

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