Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  oadp35lemc GIF version

 Description: Part of proof (3)=>(5) in Day/Pickering 1982.
Hypotheses
Ref Expression
oadp35lem.1 c0 = ((a1a2) ∩ (b1b2))
oadp35lem.2 c1 = ((a0a2) ∩ (b0b2))
oadp35lem.3 c2 = ((a0a1) ∩ (b0b1))
oadp35lem.4 p0 = ((a1b1) ∩ (a2b2))
oadp35lem.5 p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
Assertion
Ref Expression
oadp35lemc (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))

StepHypRef Expression
1 or32 82 . . 3 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = (((a0b0) ∪ (c2 ∩ (c0c1))) ∪ b1)
2 orcom 73 . . 3 (((a0b0) ∪ (c2 ∩ (c0c1))) ∪ b1) = (b1 ∪ ((a0b0) ∪ (c2 ∩ (c0c1))))
3 leo 158 . . . . . . . 8 a0 ≤ (a0a1)
4 leo 158 . . . . . . . 8 b0 ≤ (b0b1)
53, 4le2an 169 . . . . . . 7 (a0b0) ≤ ((a0a1) ∩ (b0b1))
6 oadp35lem.3 . . . . . . . 8 c2 = ((a0a1) ∩ (b0b1))
76cm 61 . . . . . . 7 ((a0a1) ∩ (b0b1)) = c2
85, 7lbtr 139 . . . . . 6 (a0b0) ≤ c2
9 leo 158 . . . . . . . . 9 a0 ≤ (a0a2)
10 leo 158 . . . . . . . . 9 b0 ≤ (b0b2)
119, 10le2an 169 . . . . . . . 8 (a0b0) ≤ ((a0a2) ∩ (b0b2))
12 oadp35lem.2 . . . . . . . . 9 c1 = ((a0a2) ∩ (b0b2))
1312cm 61 . . . . . . . 8 ((a0a2) ∩ (b0b2)) = c1
1411, 13lbtr 139 . . . . . . 7 (a0b0) ≤ c1
1514lerr 150 . . . . . 6 (a0b0) ≤ (c0c1)
168, 15ler2an 173 . . . . 5 (a0b0) ≤ (c2 ∩ (c0c1))
1716df-le2 131 . . . 4 ((a0b0) ∪ (c2 ∩ (c0c1))) = (c2 ∩ (c0c1))
1817lor 70 . . 3 (b1 ∪ ((a0b0) ∪ (c2 ∩ (c0c1)))) = (b1 ∪ (c2 ∩ (c0c1)))
191, 2, 183tr 65 . 2 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = (b1 ∪ (c2 ∩ (c0c1)))
2019lan 77 1 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))
 Colors of variables: term Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator