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

Theorem dp53lema 1161
 Description: Part of proof (5)=>(3) in Day/Pickering 1982.
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
dp53lema (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))

Proof of Theorem dp53lema
StepHypRef Expression
1 leo 158 . 2 b1 ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
2 leo 158 . . . . . 6 (b0 ∩ (a0p0)) ≤ ((b0 ∩ (a0p0)) ∪ b1)
3 dp53lem.4 . . . . . . . . 9 p0 = ((a1b1) ∩ (a2b2))
43lor 70 . . . . . . . 8 (a0p0) = (a0 ∪ ((a1b1) ∩ (a2b2)))
54lan 77 . . . . . . 7 (b0 ∩ (a0p0)) = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
6 lear 161 . . . . . . . 8 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ (a0 ∪ ((a1b1) ∩ (a2b2)))
7 lea 160 . . . . . . . . . 10 ((a1b1) ∩ (a2b2)) ≤ (a1b1)
87lelor 166 . . . . . . . . 9 (a0 ∪ ((a1b1) ∩ (a2b2))) ≤ (a0 ∪ (a1b1))
9 ax-a3 32 . . . . . . . . . 10 ((a0a1) ∪ b1) = (a0 ∪ (a1b1))
109cm 61 . . . . . . . . 9 (a0 ∪ (a1b1)) = ((a0a1) ∪ b1)
118, 10lbtr 139 . . . . . . . 8 (a0 ∪ ((a1b1) ∩ (a2b2))) ≤ ((a0a1) ∪ b1)
126, 11letr 137 . . . . . . 7 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ ((a0a1) ∪ b1)
135, 12bltr 138 . . . . . 6 (b0 ∩ (a0p0)) ≤ ((a0a1) ∪ b1)
142, 13ler2an 173 . . . . 5 (b0 ∩ (a0p0)) ≤ (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1))
15 leor 159 . . . . . . 7 b1 ≤ ((b0 ∩ (a0p0)) ∪ b1)
1615mldual2i 1125 . . . . . 6 (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1)) = ((((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) ∪ b1)
17 ancom 74 . . . . . . 7 (((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) = ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1))
1817ror 71 . . . . . 6 ((((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) ∪ b1) = (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
1916, 18tr 62 . . . . 5 (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1)) = (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
2014, 19lbtr 139 . . . 4 (b0 ∩ (a0p0)) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
211lelor 166 . . . 4 (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1))))
2220, 21letr 137 . . 3 (b0 ∩ (a0p0)) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1))))
23 lea 160 . . . . . . . 8 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (a0a1)
24 dp53lem.1 . . . . . . . . 9 c0 = ((a1a2) ∩ (b1b2))
25 dp53lem.2 . . . . . . . . 9 c1 = ((a0a2) ∩ (b0b2))
2624, 25, 3dp15 1160 . . . . . . . 8 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))
2723, 26ler2an 173 . . . . . . 7 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((a0a1) ∩ ((c0c1) ∪ (b1 ∩ (a0a1))))
28 lear 161 . . . . . . . 8 (b1 ∩ (a0a1)) ≤ (a0a1)
2928mldual2i 1125 . . . . . . 7 ((a0a1) ∩ ((c0c1) ∪ (b1 ∩ (a0a1)))) = (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1)))
3027, 29lbtr 139 . . . . . 6 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1)))
31 lea 160 . . . . . . 7 (b1 ∩ (a0a1)) ≤ b1
3231lelor 166 . . . . . 6 (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1))) ≤ (((a0a1) ∩ (c0c1)) ∪ b1)
3330, 32letr 137 . . . . 5 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a1) ∩ (c0c1)) ∪ b1)
34 orcom 73 . . . . 5 (((a0a1) ∩ (c0c1)) ∪ b1) = (b1 ∪ ((a0a1) ∩ (c0c1)))
3533, 34lbtr 139 . . . 4 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
36 leid 148 . . . 4 (b1 ∪ ((a0a1) ∩ (c0c1))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
3735, 36lel2or 170 . . 3 (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1)))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
3822, 37letr 137 . 2 (b0 ∩ (a0p0)) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
391, 38lel2or 170 1 (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (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 1120  ax-arg 1151 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:  dp53lemd  1164
 Copyright terms: Public domain W3C validator