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

Theorem dp53lemf 1168
Description: Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
Hypotheses
Ref Expression
dp53lem.1 c0 = ((a1a2) ∩ (b1b2))
dp53lem.2 c1 = ((a0a2) ∩ (b0b2))
dp53lem.3 c2 = ((a0a1) ∩ (b0b1))
dp53lem.4 p0 = ((a1b1) ∩ (a2b2))
dp53lem.5 p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
Assertion
Ref Expression
dp53lemf (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Proof of Theorem dp53lemf
StepHypRef Expression
1 leo 158 . 2 a0 ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
2 dp53lem.5 . . . . . . 7 p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
3 anass 76 . . . . . . 7 (((a0b0) ∩ (a1b1)) ∩ (a2b2)) = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
42, 3tr 62 . . . . . 6 p = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
5 dp53lem.4 . . . . . . . . . 10 p0 = ((a1b1) ∩ (a2b2))
65lan 77 . . . . . . . . 9 ((a0b0) ∩ p0) = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
76cm 61 . . . . . . . 8 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) = ((a0b0) ∩ p0)
8 leao4 165 . . . . . . . 8 ((a0b0) ∩ p0) ≤ (a0p0)
97, 8bltr 138 . . . . . . 7 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (a0p0)
10 lea 160 . . . . . . . 8 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (a0b0)
11 orcom 73 . . . . . . . 8 (a0b0) = (b0a0)
1210, 11lbtr 139 . . . . . . 7 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (b0a0)
139, 12ler2an 173 . . . . . 6 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ ((a0p0) ∩ (b0a0))
144, 13bltr 138 . . . . 5 p ≤ ((a0p0) ∩ (b0a0))
15 leo 158 . . . . . . 7 a0 ≤ (a0p0)
1615mldual2i 1127 . . . . . 6 ((a0p0) ∩ (b0a0)) = (((a0p0) ∩ b0) ∪ a0)
17 ancom 74 . . . . . . 7 ((a0p0) ∩ b0) = (b0 ∩ (a0p0))
1817ror 71 . . . . . 6 (((a0p0) ∩ b0) ∪ a0) = ((b0 ∩ (a0p0)) ∪ a0)
1916, 18tr 62 . . . . 5 ((a0p0) ∩ (b0a0)) = ((b0 ∩ (a0p0)) ∪ a0)
2014, 19lbtr 139 . . . 4 p ≤ ((b0 ∩ (a0p0)) ∪ a0)
211lelor 166 . . . 4 ((b0 ∩ (a0p0)) ∪ a0) ≤ ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))))
2220, 21letr 137 . . 3 p ≤ ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))))
23 dp53lem.1 . . . . 5 c0 = ((a1a2) ∩ (b1b2))
24 dp53lem.2 . . . . 5 c1 = ((a0a2) ∩ (b0b2))
25 dp53lem.3 . . . . 5 c2 = ((a0a1) ∩ (b0b1))
2623, 24, 25, 5, 2dp53leme 1167 . . . 4 (b0 ∩ (a0p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
2726df-le2 131 . . 3 ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))) = (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
2822, 27lbtr 139 . 2 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
291, 28lel2or 170 1 (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
Colors of variables: term
Syntax hints:   = wb 1  wle 2  wo 6  wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122  ax-arg 1153
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:  dp53lemg  1169
  Copyright terms: Public domain W3C validator