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

Theorem xxdp53 1203
Description: Part of proof (5)=>(3) 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
xxdp53 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Proof of Theorem xxdp53
StepHypRef Expression
1 leor 159 . 2 p ≤ (a0p)
2 leo 158 . . 3 a0 ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
3 xxdp.p . . . . . . . 8 p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
4 anass 76 . . . . . . . 8 (((a0b0) ∩ (a1b1)) ∩ (a2b2)) = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
53, 4tr 62 . . . . . . 7 p = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
6 xxdp.p0 . . . . . . . . . . 11 p0 = ((a1b1) ∩ (a2b2))
76lan 77 . . . . . . . . . 10 ((a0b0) ∩ p0) = ((a0b0) ∩ ((a1b1) ∩ (a2b2)))
87cm 61 . . . . . . . . 9 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) = ((a0b0) ∩ p0)
9 leao4 165 . . . . . . . . 9 ((a0b0) ∩ p0) ≤ (a0p0)
108, 9bltr 138 . . . . . . . 8 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (a0p0)
11 lea 160 . . . . . . . . 9 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (a0b0)
12 orcom 73 . . . . . . . . 9 (a0b0) = (b0a0)
1311, 12lbtr 139 . . . . . . . 8 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ (b0a0)
1410, 13ler2an 173 . . . . . . 7 ((a0b0) ∩ ((a1b1) ∩ (a2b2))) ≤ ((a0p0) ∩ (b0a0))
155, 14bltr 138 . . . . . 6 p ≤ ((a0p0) ∩ (b0a0))
16 leo 158 . . . . . . . 8 a0 ≤ (a0p0)
1716mldual2i 1127 . . . . . . 7 ((a0p0) ∩ (b0a0)) = (((a0p0) ∩ b0) ∪ a0)
18 ancom 74 . . . . . . . 8 ((a0p0) ∩ b0) = (b0 ∩ (a0p0))
1918ror 71 . . . . . . 7 (((a0p0) ∩ b0) ∪ a0) = ((b0 ∩ (a0p0)) ∪ a0)
2017, 19tr 62 . . . . . 6 ((a0p0) ∩ (b0a0)) = ((b0 ∩ (a0p0)) ∪ a0)
2115, 20lbtr 139 . . . . 5 p ≤ ((b0 ∩ (a0p0)) ∪ a0)
222lelor 166 . . . . 5 ((b0 ∩ (a0p0)) ∪ a0) ≤ ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))))
2321, 22letr 137 . . . 4 p ≤ ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))))
24 lea 160 . . . . . . . 8 (b0 ∩ (a0p0)) ≤ b0
25 leor 159 . . . . . . . . 9 (b0 ∩ (a0p0)) ≤ (b1 ∪ (b0 ∩ (a0p0)))
26 leo 158 . . . . . . . . . 10 b1 ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
27 leo 158 . . . . . . . . . . . . . 14 (b0 ∩ (a0p0)) ≤ ((b0 ∩ (a0p0)) ∪ b1)
286lor 70 . . . . . . . . . . . . . . . 16 (a0p0) = (a0 ∪ ((a1b1) ∩ (a2b2)))
2928lan 77 . . . . . . . . . . . . . . 15 (b0 ∩ (a0p0)) = (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2))))
30 lear 161 . . . . . . . . . . . . . . . 16 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ (a0 ∪ ((a1b1) ∩ (a2b2)))
31 lea 160 . . . . . . . . . . . . . . . . . 18 ((a1b1) ∩ (a2b2)) ≤ (a1b1)
3231lelor 166 . . . . . . . . . . . . . . . . 17 (a0 ∪ ((a1b1) ∩ (a2b2))) ≤ (a0 ∪ (a1b1))
33 ax-a3 32 . . . . . . . . . . . . . . . . . 18 ((a0a1) ∪ b1) = (a0 ∪ (a1b1))
3433cm 61 . . . . . . . . . . . . . . . . 17 (a0 ∪ (a1b1)) = ((a0a1) ∪ b1)
3532, 34lbtr 139 . . . . . . . . . . . . . . . 16 (a0 ∪ ((a1b1) ∩ (a2b2))) ≤ ((a0a1) ∪ b1)
3630, 35letr 137 . . . . . . . . . . . . . . 15 (b0 ∩ (a0 ∪ ((a1b1) ∩ (a2b2)))) ≤ ((a0a1) ∪ b1)
3729, 36bltr 138 . . . . . . . . . . . . . 14 (b0 ∩ (a0p0)) ≤ ((a0a1) ∪ b1)
3827, 37ler2an 173 . . . . . . . . . . . . 13 (b0 ∩ (a0p0)) ≤ (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1))
39 leor 159 . . . . . . . . . . . . . . 15 b1 ≤ ((b0 ∩ (a0p0)) ∪ b1)
4039mldual2i 1127 . . . . . . . . . . . . . 14 (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1)) = ((((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) ∪ b1)
41 ancom 74 . . . . . . . . . . . . . . 15 (((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) = ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1))
4241ror 71 . . . . . . . . . . . . . 14 ((((b0 ∩ (a0p0)) ∪ b1) ∩ (a0a1)) ∪ b1) = (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
4340, 42tr 62 . . . . . . . . . . . . 13 (((b0 ∩ (a0p0)) ∪ b1) ∩ ((a0a1) ∪ b1)) = (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
4438, 43lbtr 139 . . . . . . . . . . . 12 (b0 ∩ (a0p0)) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1)
4526lelor 166 . . . . . . . . . . . 12 (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ b1) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1))))
4644, 45letr 137 . . . . . . . . . . 11 (b0 ∩ (a0p0)) ≤ (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1))))
47 lea 160 . . . . . . . . . . . . . . . 16 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (a0a1)
48 xxdp.c0 . . . . . . . . . . . . . . . . 17 c0 = ((a1a2) ∩ (b1b2))
49 xxdp.c1 . . . . . . . . . . . . . . . . 17 c1 = ((a0a2) ∩ (b0b2))
5048, 49, 6dp15 1162 . . . . . . . . . . . . . . . 16 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))
5147, 50ler2an 173 . . . . . . . . . . . . . . 15 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((a0a1) ∩ ((c0c1) ∪ (b1 ∩ (a0a1))))
52 lear 161 . . . . . . . . . . . . . . . 16 (b1 ∩ (a0a1)) ≤ (a0a1)
5352mldual2i 1127 . . . . . . . . . . . . . . 15 ((a0a1) ∩ ((c0c1) ∪ (b1 ∩ (a0a1)))) = (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1)))
5451, 53lbtr 139 . . . . . . . . . . . . . 14 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1)))
55 lea 160 . . . . . . . . . . . . . . 15 (b1 ∩ (a0a1)) ≤ b1
5655lelor 166 . . . . . . . . . . . . . 14 (((a0a1) ∩ (c0c1)) ∪ (b1 ∩ (a0a1))) ≤ (((a0a1) ∩ (c0c1)) ∪ b1)
5754, 56letr 137 . . . . . . . . . . . . 13 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (((a0a1) ∩ (c0c1)) ∪ b1)
58 orcom 73 . . . . . . . . . . . . 13 (((a0a1) ∩ (c0c1)) ∪ b1) = (b1 ∪ ((a0a1) ∩ (c0c1)))
5957, 58lbtr 139 . . . . . . . . . . . 12 ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
60 leid 148 . . . . . . . . . . . 12 (b1 ∪ ((a0a1) ∩ (c0c1))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
6159, 60lel2or 170 . . . . . . . . . . 11 (((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ∪ (b1 ∪ ((a0a1) ∩ (c0c1)))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
6246, 61letr 137 . . . . . . . . . 10 (b0 ∩ (a0p0)) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
6326, 62lel2or 170 . . . . . . . . 9 (b1 ∪ (b0 ∩ (a0p0))) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
6425, 63letr 137 . . . . . . . 8 (b0 ∩ (a0p0)) ≤ (b1 ∪ ((a0a1) ∩ (c0c1)))
6524, 64ler2an 173 . . . . . . 7 (b0 ∩ (a0p0)) ≤ (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
66 or32 82 . . . . . . . . . . 11 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = (((a0b0) ∪ (c2 ∩ (c0c1))) ∪ b1)
67 orcom 73 . . . . . . . . . . 11 (((a0b0) ∪ (c2 ∩ (c0c1))) ∪ b1) = (b1 ∪ ((a0b0) ∪ (c2 ∩ (c0c1))))
68 leo 158 . . . . . . . . . . . . . . . 16 a0 ≤ (a0a1)
69 leo 158 . . . . . . . . . . . . . . . 16 b0 ≤ (b0b1)
7068, 69le2an 169 . . . . . . . . . . . . . . 15 (a0b0) ≤ ((a0a1) ∩ (b0b1))
71 xxdp.c2 . . . . . . . . . . . . . . . 16 c2 = ((a0a1) ∩ (b0b1))
7271cm 61 . . . . . . . . . . . . . . 15 ((a0a1) ∩ (b0b1)) = c2
7370, 72lbtr 139 . . . . . . . . . . . . . 14 (a0b0) ≤ c2
74 leo 158 . . . . . . . . . . . . . . . . 17 a0 ≤ (a0a2)
75 leo 158 . . . . . . . . . . . . . . . . 17 b0 ≤ (b0b2)
7674, 75le2an 169 . . . . . . . . . . . . . . . 16 (a0b0) ≤ ((a0a2) ∩ (b0b2))
7749cm 61 . . . . . . . . . . . . . . . 16 ((a0a2) ∩ (b0b2)) = c1
7876, 77lbtr 139 . . . . . . . . . . . . . . 15 (a0b0) ≤ c1
7978lerr 150 . . . . . . . . . . . . . 14 (a0b0) ≤ (c0c1)
8073, 79ler2an 173 . . . . . . . . . . . . 13 (a0b0) ≤ (c2 ∩ (c0c1))
8180df-le2 131 . . . . . . . . . . . 12 ((a0b0) ∪ (c2 ∩ (c0c1))) = (c2 ∩ (c0c1))
8281lor 70 . . . . . . . . . . 11 (b1 ∪ ((a0b0) ∪ (c2 ∩ (c0c1)))) = (b1 ∪ (c2 ∩ (c0c1)))
8366, 67, 823tr 65 . . . . . . . . . 10 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = (b1 ∪ (c2 ∩ (c0c1)))
8483lan 77 . . . . . . . . 9 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))
8571ran 78 . . . . . . . . . . . . . 14 (c2 ∩ (c0c1)) = (((a0a1) ∩ (b0b1)) ∩ (c0c1))
86 an32 83 . . . . . . . . . . . . . 14 (((a0a1) ∩ (b0b1)) ∩ (c0c1)) = (((a0a1) ∩ (c0c1)) ∩ (b0b1))
8785, 86tr 62 . . . . . . . . . . . . 13 (c2 ∩ (c0c1)) = (((a0a1) ∩ (c0c1)) ∩ (b0b1))
8887lor 70 . . . . . . . . . . . 12 (b1 ∪ (c2 ∩ (c0c1))) = (b1 ∪ (((a0a1) ∩ (c0c1)) ∩ (b0b1)))
89 leor 159 . . . . . . . . . . . . 13 b1 ≤ (b0b1)
9089ml2i 1125 . . . . . . . . . . . 12 (b1 ∪ (((a0a1) ∩ (c0c1)) ∩ (b0b1))) = ((b1 ∪ ((a0a1) ∩ (c0c1))) ∩ (b0b1))
91 ancom 74 . . . . . . . . . . . 12 ((b1 ∪ ((a0a1) ∩ (c0c1))) ∩ (b0b1)) = ((b0b1) ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
9288, 90, 913tr 65 . . . . . . . . . . 11 (b1 ∪ (c2 ∩ (c0c1))) = ((b0b1) ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
9392lan 77 . . . . . . . . . 10 (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) = (b0 ∩ ((b0b1) ∩ (b1 ∪ ((a0a1) ∩ (c0c1)))))
94 anass 76 . . . . . . . . . . 11 ((b0 ∩ (b0b1)) ∩ (b1 ∪ ((a0a1) ∩ (c0c1)))) = (b0 ∩ ((b0b1) ∩ (b1 ∪ ((a0a1) ∩ (c0c1)))))
9594cm 61 . . . . . . . . . 10 (b0 ∩ ((b0b1) ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))) = ((b0 ∩ (b0b1)) ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
96 anabs 121 . . . . . . . . . . 11 (b0 ∩ (b0b1)) = b0
9796ran 78 . . . . . . . . . 10 ((b0 ∩ (b0b1)) ∩ (b1 ∪ ((a0a1) ∩ (c0c1)))) = (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
9893, 95, 973tr 65 . . . . . . . . 9 (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
9984, 98tr 62 . . . . . . . 8 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1))))
10099cm 61 . . . . . . 7 (b0 ∩ (b1 ∪ ((a0a1) ∩ (c0c1)))) = (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))
10165, 100lbtr 139 . . . . . 6 (b0 ∩ (a0p0)) ≤ (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))))
102 orass 75 . . . . . . . . . 10 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = ((a0b0) ∪ (b1 ∪ (c2 ∩ (c0c1))))
103 orcom 73 . . . . . . . . . 10 ((a0b0) ∪ (b1 ∪ (c2 ∩ (c0c1)))) = ((b1 ∪ (c2 ∩ (c0c1))) ∪ (a0b0))
104102, 103tr 62 . . . . . . . . 9 (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1))) = ((b1 ∪ (c2 ∩ (c0c1))) ∪ (a0b0))
105104lan 77 . . . . . . . 8 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ ((b1 ∪ (c2 ∩ (c0c1))) ∪ (a0b0)))
106 lear 161 . . . . . . . . 9 (a0b0) ≤ b0
107106mldual2i 1127 . . . . . . . 8 (b0 ∩ ((b1 ∪ (c2 ∩ (c0c1))) ∪ (a0b0))) = ((b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) ∪ (a0b0))
108 orcom 73 . . . . . . . 8 ((b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))) ∪ (a0b0)) = ((a0b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
109105, 107, 1083tr 65 . . . . . . 7 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = ((a0b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
110 lea 160 . . . . . . . 8 (a0b0) ≤ a0
111110leror 152 . . . . . . 7 ((a0b0) ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
112109, 111bltr 138 . . . . . 6 (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
113101, 112letr 137 . . . . 5 (b0 ∩ (a0p0)) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
114113df-le2 131 . . . 4 ((b0 ∩ (a0p0)) ∪ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))) = (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
11523, 114lbtr 139 . . 3 p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
1162, 115lel2or 170 . 2 (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))
1171, 116letr 137 1 p ≤ (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: (None)
  Copyright terms: Public domain W3C validator