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

Theorem xdp15 1197
Description: Part of proof (1)=>(5) in Day/Pickering 1982.
Hypotheses
Ref Expression
xdp15.d d = (a2 v (a0 ^ (a1 v b1)))
xdp15.p0 p0 = ((a1 v b1) ^ (a2 v b2))
xdp15.e e = (b0 ^ (a0 v p0))
xdp15.c0 c0 = ((a1 v a2) ^ (b1 v b2))
xdp15.c1 c1 = ((a0 v a2) ^ (b0 v b2))
Assertion
Ref Expression
xdp15 ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< ((c0 v c1) v (b1 ^ (a0 v a1)))

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