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

Theorem xxdp15 1202
Description: Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
Hypotheses
Ref Expression
xxdp.1 p2 ≤ (a2b2)
xxdp.c0 c0 = ((a1a2) ∩ (b1b2))
xxdp.c1 c1 = ((a0a2) ∩ (b0b2))
xxdp.c2 c2 = ((a0a1) ∩ (b0b1))
xxdp.d d = (a2 ∪ (a0 ∩ (a1b1)))
xxdp.e e = (b0 ∩ (a0p0))
xxdp.p p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
xxdp.p0 p0 = ((a1b1) ∩ (a2b2))
xxdp.p2 p2 = ((a0b0) ∩ (a1b1))
Assertion
Ref Expression
xxdp15 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Proof of Theorem xxdp15
StepHypRef Expression
1 xxdp.e . . . . . . . . . . 11 e = (b0 ∩ (a0p0))
2 xxdp.p0 . . . . . . . . . . . . 13 p0 = ((a1b1) ∩ (a2b2))
32lor 70 . . . . . . . . . . . 12 (a0p0) = (a0 ∪ ((a1b1) ∩ (a2b2)))
43lan 77 . . . . . . . . . . 11 (b0 ∩ (a0p0)) = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
51, 4tr 62 . . . . . . . . . 10 e = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
65lor 70 . . . . . . . . 9 (a0e) = (a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))))
76ran 78 . . . . . . . 8 ((a0e) ∩ (a1b1)) = ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1))
8 le1 146 . . . . . . . . . . . 12 b0 ≤ 1
98leran 153 . . . . . . . . . . 11 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
109lelor 166 . . . . . . . . . 10 (a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ≤ (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))))
1110leran 153 . . . . . . . . 9 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1))
12 an1r 107 . . . . . . . . . . . . . . 15 (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) = (a0 ∪ ((a1b1) ∩ (a2b2)))
1312lor 70 . . . . . . . . . . . . . 14 (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) = (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2))))
14 orass 75 . . . . . . . . . . . . . . 15 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2))))
1514cm 61 . . . . . . . . . . . . . 14 (a0 ∪ (a0 ∪ ((a1b1) ∩ (a2b2)))) = ((a0a0) ∪ ((a1b1) ∩ (a2b2)))
16 oridm 110 . . . . . . . . . . . . . . . 16 (a0a0) = a0
1716ror 71 . . . . . . . . . . . . . . 15 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (a0 ∪ ((a1b1) ∩ (a2b2)))
18 orcom 73 . . . . . . . . . . . . . . 15 (a0 ∪ ((a1b1) ∩ (a2b2))) = (((a1b1) ∩ (a2b2)) ∪ a0)
1917, 18tr 62 . . . . . . . . . . . . . 14 ((a0a0) ∪ ((a1b1) ∩ (a2b2))) = (((a1b1) ∩ (a2b2)) ∪ a0)
2013, 15, 193tr 65 . . . . . . . . . . . . 13 (a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) = (((a1b1) ∩ (a2b2)) ∪ a0)
2120ran 78 . . . . . . . . . . . 12 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) = ((((a1b1) ∩ (a2b2)) ∪ a0) ∩ (a1b1))
22 lea 160 . . . . . . . . . . . . 13 ((a1b1) ∩ (a2b2)) ≤ (a1b1)
2322mlduali 1128 . . . . . . . . . . . 12 ((((a1b1) ∩ (a2b2)) ∪ a0) ∩ (a1b1)) = (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1)))
2421, 23tr 62 . . . . . . . . . . 11 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) = (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1)))
25 lear 161 . . . . . . . . . . . 12 ((a1b1) ∩ (a2b2)) ≤ (a2b2)
2625leror 152 . . . . . . . . . . 11 (((a1b1) ∩ (a2b2)) ∪ (a0 ∩ (a1b1))) ≤ ((a2b2) ∪ (a0 ∩ (a1b1)))
2724, 26bltr 138 . . . . . . . . . 10 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ ((a2b2) ∪ (a0 ∩ (a1b1)))
28 or32 82 . . . . . . . . . . 11 ((a2b2) ∪ (a0 ∩ (a1b1))) = ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2)
29 xxdp.d . . . . . . . . . . . . 13 d = (a2 ∪ (a0 ∩ (a1b1)))
3029ror 71 . . . . . . . . . . . 12 (db2) = ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2)
3130cm 61 . . . . . . . . . . 11 ((a2 ∪ (a0 ∩ (a1b1))) ∪ b2) = (db2)
3228, 31tr 62 . . . . . . . . . 10 ((a2b2) ∪ (a0 ∩ (a1b1))) = (db2)
3327, 32lbtr 139 . . . . . . . . 9 ((a0 ∪ (1 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ (db2)
3411, 33letr 137 . . . . . . . 8 ((a0 ∪ (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))) ∩ (a1b1)) ≤ (db2)
357, 34bltr 138 . . . . . . 7 ((a0e) ∩ (a1b1)) ≤ (db2)
3635ax-arg 1153 . . . . . 6 ((a0a1) ∩ (eb1)) ≤ (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2)))
371ror 71 . . . . . . 7 (eb1) = ((b0 ∩ (a0p0)) ∪ b1)
3837lan 77 . . . . . 6 ((a0a1) ∩ (eb1)) = ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1))
3929lor 70 . . . . . . . 8 (a0d) = (a0 ∪ (a2 ∪ (a0 ∩ (a1b1))))
401ror 71 . . . . . . . 8 (eb2) = ((b0 ∩ (a0p0)) ∪ b2)
4139, 402an 79 . . . . . . 7 ((a0d) ∩ (eb2)) = ((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2))
4229lor 70 . . . . . . . 8 (a1d) = (a1 ∪ (a2 ∪ (a0 ∩ (a1b1))))
4342ran 78 . . . . . . 7 ((a1d) ∩ (b1b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))
4441, 432or 72 . . . . . 6 (((a0d) ∩ (eb2)) ∪ ((a1d) ∩ (b1b2))) = (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)))
4536, 38, 44le3tr2 141 . . . . 5 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)))
46 or12 80 . . . . . . . 8 (a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) = (a2 ∪ (a0 ∪ (a0 ∩ (a1b1))))
47 orabs 120 . . . . . . . . 9 (a0 ∪ (a0 ∩ (a1b1))) = a0
4847lor 70 . . . . . . . 8 (a2 ∪ (a0 ∪ (a0 ∩ (a1b1)))) = (a2a0)
49 orcom 73 . . . . . . . 8 (a2a0) = (a0a2)
5046, 48, 493tr 65 . . . . . . 7 (a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) = (a0a2)
5150ran 78 . . . . . 6 ((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) = ((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2))
52 orass 75 . . . . . . . 8 ((a1a2) ∪ (a0 ∩ (a1b1))) = (a1 ∪ (a2 ∪ (a0 ∩ (a1b1))))
5352ran 78 . . . . . . 7 (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)) = ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))
5453cm 61 . . . . . 6 ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2)) = (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2))
5551, 542or 72 . . . . 5 (((a0 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ ((a1 ∪ (a2 ∪ (a0 ∩ (a1b1)))) ∩ (b1b2))) = (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)))
5645, 55lbtr 139 . . . 4 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)))
57 ax-a2 31 . . . . . . . . . 10 (a1a2) = (a2a1)
58 ax-a2 31 . . . . . . . . . . 11 (a1b1) = (b1a1)
5958lan 77 . . . . . . . . . 10 (a0 ∩ (a1b1)) = (a0 ∩ (b1a1))
6057, 592or 72 . . . . . . . . 9 ((a1a2) ∪ (a0 ∩ (a1b1))) = ((a2a1) ∪ (a0 ∩ (b1a1)))
61 orass 75 . . . . . . . . 9 ((a2a1) ∪ (a0 ∩ (b1a1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1a1))))
6260, 61tr 62 . . . . . . . 8 ((a1a2) ∪ (a0 ∩ (a1b1))) = (a2 ∪ (a1 ∪ (a0 ∩ (b1a1))))
63 ml3le 1129 . . . . . . . . 9 (a1 ∪ (a0 ∩ (b1a1))) ≤ (a1 ∪ (b1 ∩ (a0a1)))
6463lelor 166 . . . . . . . 8 (a2 ∪ (a1 ∪ (a0 ∩ (b1a1)))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
6562, 64bltr 138 . . . . . . 7 ((a1a2) ∪ (a0 ∩ (a1b1))) ≤ (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
66 orass 75 . . . . . . . . 9 ((a2a1) ∪ (b1 ∩ (a0a1))) = (a2 ∪ (a1 ∪ (b1 ∩ (a0a1))))
6766cm 61 . . . . . . . 8 (a2 ∪ (a1 ∪ (b1 ∩ (a0a1)))) = ((a2a1) ∪ (b1 ∩ (a0a1)))
68 ax-a2 31 . . . . . . . . 9 (a2a1) = (a1a2)
6968ror 71 . . . . . . . 8 ((a2a1) ∪ (b1 ∩ (a0a1))) = ((a1a2) ∪ (b1 ∩ (a0a1)))
7067, 69tr 62 . . . . . . 7 (a2 ∪ (a1 ∪ (b1 ∩ (a0a1)))) = ((a1a2) ∪ (b1 ∩ (a0a1)))
7165, 70lbtr 139 . . . . . 6 ((a1a2) ∪ (a0 ∩ (a1b1))) ≤ ((a1a2) ∪ (b1 ∩ (a0a1)))
7271leran 153 . . . . 5 (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2)) ≤ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))
7372lelor 166 . . . 4 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (a0 ∩ (a1b1))) ∩ (b1b2))) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)))
7456, 73letr 137 . . 3 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)))
75 lea 160 . . . . . . 7 (b0 ∩ (a0p0)) ≤ b0
7675leror 152 . . . . . 6 ((b0 ∩ (a0p0)) ∪ b2) ≤ (b0b2)
7776lelan 167 . . . . 5 ((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ≤ ((a0a2) ∩ (b0b2))
78 leao1 162 . . . . . . . 8 (b1 ∩ (a0a1)) ≤ (b1b2)
7978mldual2i 1127 . . . . . . 7 ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) = (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1)))
80 ancom 74 . . . . . . 7 ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))
81 ancom 74 . . . . . . . 8 ((b1b2) ∩ (a1a2)) = ((a1a2) ∩ (b1b2))
8281ror 71 . . . . . . 7 (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) = (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
8379, 80, 823tr2 64 . . . . . 6 (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)) = (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
8483bile 142 . . . . 5 (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2)) ≤ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))
8577, 84le2or 168 . . . 4 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))) ≤ (((a0a2) ∩ (b0b2)) ∪ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1))))
86 or12 80 . . . 4 (((a0a2) ∩ (b0b2)) ∪ (((a1a2) ∩ (b1b2)) ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
8785, 86lbtr 139 . . 3 (((a0a2) ∩ ((b0 ∩ (a0p0)) ∪ b2)) ∪ (((a1a2) ∪ (b1 ∩ (a0a1))) ∩ (b1b2))) ≤ (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
8874, 87letr 137 . 2 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
89 xxdp.c0 . . . . 5 c0 = ((a1a2) ∩ (b1b2))
90 xxdp.c1 . . . . . 6 c1 = ((a0a2) ∩ (b0b2))
9190ror 71 . . . . 5 (c1 ∪ (b1 ∩ (a0a1))) = (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))
9289, 912or 72 . . . 4 (c0 ∪ (c1 ∪ (b1 ∩ (a0a1)))) = (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1))))
9392cm 61 . . 3 (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0a1))))
94 orass 75 . . . 4 ((c0c1) ∪ (b1 ∩ (a0a1))) = (c0 ∪ (c1 ∪ (b1 ∩ (a0a1))))
9594cm 61 . . 3 (c0 ∪ (c1 ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ (b1 ∩ (a0a1)))
9693, 95tr 62 . 2 (((a1a2) ∩ (b1b2)) ∪ (((a0a2) ∩ (b0b2)) ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ (b1 ∩ (a0a1)))
9788, 96lbtr 139 1 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))
Colors of variables: term
Syntax hints:   = wb 1  wle 2  wo 6  wa 7  1wt 8
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: (None)
  Copyright terms: Public domain W3C validator