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

Theorem xxdp41 1201
Description: Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-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
xxdp41 c2 ≤ (c0c1)

Proof of Theorem xxdp41
StepHypRef Expression
1 xxdp.c2 . . . . . . . . . . . 12 c2 = ((a0a1) ∩ (b0b1))
2 ancom 74 . . . . . . . . . . . 12 ((a0a1) ∩ (b0b1)) = ((b0b1) ∩ (a0a1))
31, 2tr 62 . . . . . . . . . . 11 c2 = ((b0b1) ∩ (a0a1))
4 leor 159 . . . . . . . . . . . . 13 b0 ≤ (a0b0)
54leror 152 . . . . . . . . . . . 12 (b0b1) ≤ ((a0b0) ∪ b1)
6 leo 158 . . . . . . . . . . . 12 (a0a1) ≤ ((a0a1) ∪ b1)
75, 6le2an 169 . . . . . . . . . . 11 ((b0b1) ∩ (a0a1)) ≤ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1))
83, 7bltr 138 . . . . . . . . . 10 c2 ≤ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1))
98df2le2 136 . . . . . . . . 9 (c2 ∩ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1))) = c2
109cm 61 . . . . . . . 8 c2 = (c2 ∩ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)))
11 anass 76 . . . . . . . . 9 ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1)) = (c2 ∩ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)))
1211cm 61 . . . . . . . 8 (c2 ∩ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1))) = ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1))
1310, 12tr 62 . . . . . . 7 c2 = ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1))
14 ax-a2 31 . . . . . . . . . . . . . . . 16 (a0a1) = (a1a0)
1514ror 71 . . . . . . . . . . . . . . 15 ((a0a1) ∪ b1) = ((a1a0) ∪ b1)
16 or32 82 . . . . . . . . . . . . . . 15 ((a1a0) ∪ b1) = ((a1b1) ∪ a0)
1715, 16tr 62 . . . . . . . . . . . . . 14 ((a0a1) ∪ b1) = ((a1b1) ∪ a0)
1817lan 77 . . . . . . . . . . . . 13 (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) = (((a0b0) ∪ b1) ∩ ((a1b1) ∪ a0))
19 ancom 74 . . . . . . . . . . . . 13 (((a0b0) ∪ b1) ∩ ((a1b1) ∪ a0)) = (((a1b1) ∪ a0) ∩ ((a0b0) ∪ b1))
2018, 19tr 62 . . . . . . . . . . . 12 (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) = (((a1b1) ∪ a0) ∩ ((a0b0) ∪ b1))
21 leor 159 . . . . . . . . . . . . . 14 b1 ≤ (a1b1)
2221ler 149 . . . . . . . . . . . . 13 b1 ≤ ((a1b1) ∪ a0)
2322mldual2i 1127 . . . . . . . . . . . 12 (((a1b1) ∪ a0) ∩ ((a0b0) ∪ b1)) = ((((a1b1) ∪ a0) ∩ (a0b0)) ∪ b1)
24 ancom 74 . . . . . . . . . . . . . 14 (((a1b1) ∪ a0) ∩ (a0b0)) = ((a0b0) ∩ ((a1b1) ∪ a0))
25 leo 158 . . . . . . . . . . . . . . 15 a0 ≤ (a0b0)
2625mldual2i 1127 . . . . . . . . . . . . . 14 ((a0b0) ∩ ((a1b1) ∪ a0)) = (((a0b0) ∩ (a1b1)) ∪ a0)
2724, 26tr 62 . . . . . . . . . . . . 13 (((a1b1) ∪ a0) ∩ (a0b0)) = (((a0b0) ∩ (a1b1)) ∪ a0)
2827ror 71 . . . . . . . . . . . 12 ((((a1b1) ∪ a0) ∩ (a0b0)) ∪ b1) = ((((a0b0) ∩ (a1b1)) ∪ a0) ∪ b1)
2920, 23, 283tr 65 . . . . . . . . . . 11 (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) = ((((a0b0) ∩ (a1b1)) ∪ a0) ∪ b1)
30 orass 75 . . . . . . . . . . 11 ((((a0b0) ∩ (a1b1)) ∪ a0) ∪ b1) = (((a0b0) ∩ (a1b1)) ∪ (a0b1))
31 orcom 73 . . . . . . . . . . 11 (((a0b0) ∩ (a1b1)) ∪ (a0b1)) = ((a0b1) ∪ ((a0b0) ∩ (a1b1)))
3229, 30, 313tr 65 . . . . . . . . . 10 (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) = ((a0b1) ∪ ((a0b0) ∩ (a1b1)))
33 leo 158 . . . . . . . . . . 11 (a0b1) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))
34 xxdp.p2 . . . . . . . . . . . . . . . . 17 p2 = ((a0b0) ∩ (a1b1))
3534cm 61 . . . . . . . . . . . . . . . 16 ((a0b0) ∩ (a1b1)) = p2
36 xxdp.1 . . . . . . . . . . . . . . . 16 p2 ≤ (a2b2)
3735, 36bltr 138 . . . . . . . . . . . . . . 15 ((a0b0) ∩ (a1b1)) ≤ (a2b2)
3837df2le2 136 . . . . . . . . . . . . . 14 (((a0b0) ∩ (a1b1)) ∩ (a2b2)) = ((a0b0) ∩ (a1b1))
3938cm 61 . . . . . . . . . . . . 13 ((a0b0) ∩ (a1b1)) = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
40 xxdp.p . . . . . . . . . . . . . 14 p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))
4140cm 61 . . . . . . . . . . . . 13 (((a0b0) ∩ (a1b1)) ∩ (a2b2)) = p
4239, 41tr 62 . . . . . . . . . . . 12 ((a0b0) ∩ (a1b1)) = p
43 xxdp.c0 . . . . . . . . . . . . 13 c0 = ((a1a2) ∩ (b1b2))
44 xxdp.c1 . . . . . . . . . . . . 13 c1 = ((a0a2) ∩ (b0b2))
4543, 44, 1, 40dp34 1181 . . . . . . . . . . . 12 p ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))
4642, 45bltr 138 . . . . . . . . . . 11 ((a0b0) ∩ (a1b1)) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))
4733, 46lel2or 170 . . . . . . . . . 10 ((a0b1) ∪ ((a0b0) ∩ (a1b1))) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))
4832, 47bltr 138 . . . . . . . . 9 (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1)) ≤ ((a0b1) ∪ (c2 ∩ (c0c1)))
4948lelan 167 . . . . . . . 8 (c2 ∩ (((a0b0) ∪ b1) ∩ ((a0a1) ∪ b1))) ≤ (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1))))
5011, 49bltr 138 . . . . . . 7 ((c2 ∩ ((a0b0) ∪ b1)) ∩ ((a0a1) ∪ b1)) ≤ (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1))))
5113, 50bltr 138 . . . . . 6 c2 ≤ (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1))))
52 mldual 1124 . . . . . . 7 (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1)))) = ((c2 ∩ (a0b1)) ∪ (c2 ∩ (c0c1)))
53 ancom 74 . . . . . . . 8 (c2 ∩ (c0c1)) = ((c0c1) ∩ c2)
5453lor 70 . . . . . . 7 ((c2 ∩ (a0b1)) ∪ (c2 ∩ (c0c1))) = ((c2 ∩ (a0b1)) ∪ ((c0c1) ∩ c2))
55 lea 160 . . . . . . . . 9 (c2 ∩ (a0b1)) ≤ c2
5655ml2i 1125 . . . . . . . 8 ((c2 ∩ (a0b1)) ∪ ((c0c1) ∩ c2)) = (((c2 ∩ (a0b1)) ∪ (c0c1)) ∩ c2)
57 ancom 74 . . . . . . . 8 (((c2 ∩ (a0b1)) ∪ (c0c1)) ∩ c2) = (c2 ∩ ((c2 ∩ (a0b1)) ∪ (c0c1)))
58 ax-a2 31 . . . . . . . . 9 ((c2 ∩ (a0b1)) ∪ (c0c1)) = ((c0c1) ∪ (c2 ∩ (a0b1)))
5958lan 77 . . . . . . . 8 (c2 ∩ ((c2 ∩ (a0b1)) ∪ (c0c1))) = (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1))))
6056, 57, 593tr 65 . . . . . . 7 ((c2 ∩ (a0b1)) ∪ ((c0c1) ∩ c2)) = (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1))))
6152, 54, 603tr 65 . . . . . 6 (c2 ∩ ((a0b1) ∪ (c2 ∩ (c0c1)))) = (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1))))
6251, 61lbtr 139 . . . . 5 c2 ≤ (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1))))
63 mldual 1124 . . . . . . 7 (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1)))) = ((c2 ∩ (c0c1)) ∪ (c2 ∩ (a0b1)))
641ran 78 . . . . . . . . 9 (c2 ∩ (a0b1)) = (((a0a1) ∩ (b0b1)) ∩ (a0b1))
65 anass 76 . . . . . . . . 9 (((a0a1) ∩ (b0b1)) ∩ (a0b1)) = ((a0a1) ∩ ((b0b1) ∩ (a0b1)))
66 leor 159 . . . . . . . . . . . . 13 b1 ≤ (b0b1)
6766mldual2i 1127 . . . . . . . . . . . 12 ((b0b1) ∩ (a0b1)) = (((b0b1) ∩ a0) ∪ b1)
68 orcom 73 . . . . . . . . . . . 12 (((b0b1) ∩ a0) ∪ b1) = (b1 ∪ ((b0b1) ∩ a0))
69 ancom 74 . . . . . . . . . . . . 13 ((b0b1) ∩ a0) = (a0 ∩ (b0b1))
7069lor 70 . . . . . . . . . . . 12 (b1 ∪ ((b0b1) ∩ a0)) = (b1 ∪ (a0 ∩ (b0b1)))
7167, 68, 703tr 65 . . . . . . . . . . 11 ((b0b1) ∩ (a0b1)) = (b1 ∪ (a0 ∩ (b0b1)))
7271lan 77 . . . . . . . . . 10 ((a0a1) ∩ ((b0b1) ∩ (a0b1))) = ((a0a1) ∩ (b1 ∪ (a0 ∩ (b0b1))))
73 leao1 162 . . . . . . . . . . 11 (a0 ∩ (b0b1)) ≤ (a0a1)
7473mldual2i 1127 . . . . . . . . . 10 ((a0a1) ∩ (b1 ∪ (a0 ∩ (b0b1)))) = (((a0a1) ∩ b1) ∪ (a0 ∩ (b0b1)))
75 orcom 73 . . . . . . . . . . 11 (((a0a1) ∩ b1) ∪ (a0 ∩ (b0b1))) = ((a0 ∩ (b0b1)) ∪ ((a0a1) ∩ b1))
76 ancom 74 . . . . . . . . . . . 12 ((a0a1) ∩ b1) = (b1 ∩ (a0a1))
7776lor 70 . . . . . . . . . . 11 ((a0 ∩ (b0b1)) ∪ ((a0a1) ∩ b1)) = ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))
7875, 77tr 62 . . . . . . . . . 10 (((a0a1) ∩ b1) ∪ (a0 ∩ (b0b1))) = ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))
7972, 74, 783tr 65 . . . . . . . . 9 ((a0a1) ∩ ((b0b1) ∩ (a0b1))) = ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))
8064, 65, 793tr 65 . . . . . . . 8 (c2 ∩ (a0b1)) = ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))
8180lor 70 . . . . . . 7 ((c2 ∩ (c0c1)) ∪ (c2 ∩ (a0b1))) = ((c2 ∩ (c0c1)) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))
8263, 81tr 62 . . . . . 6 (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1)))) = ((c2 ∩ (c0c1)) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))
83 lear 161 . . . . . . 7 (c2 ∩ (c0c1)) ≤ (c0c1)
8483leror 152 . . . . . 6 ((c2 ∩ (c0c1)) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))) ≤ ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))
8582, 84bltr 138 . . . . 5 (c2 ∩ ((c0c1) ∪ (c2 ∩ (a0b1)))) ≤ ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))
8662, 85letr 137 . . . 4 c2 ≤ ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))))
87 orcom 73 . . . . . . 7 ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1))) = ((b1 ∩ (a0a1)) ∪ (a0 ∩ (b0b1)))
8887lor 70 . . . . . 6 ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))) = ((c0c1) ∪ ((b1 ∩ (a0a1)) ∪ (a0 ∩ (b0b1))))
89 or4 84 . . . . . . 7 ((c0c1) ∪ ((b1 ∩ (a0a1)) ∪ (a0 ∩ (b0b1)))) = ((c0 ∪ (b1 ∩ (a0a1))) ∪ (c1 ∪ (a0 ∩ (b0b1))))
90 ancom 74 . . . . . . . . . 10 ((a1a2) ∩ (b1b2)) = ((b1b2) ∩ (a1a2))
9143, 90tr 62 . . . . . . . . 9 c0 = ((b1b2) ∩ (a1a2))
9291ror 71 . . . . . . . 8 (c0 ∪ (b1 ∩ (a0a1))) = (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1)))
9344ror 71 . . . . . . . 8 (c1 ∪ (a0 ∩ (b0b1))) = (((a0a2) ∩ (b0b2)) ∪ (a0 ∩ (b0b1)))
9492, 932or 72 . . . . . . 7 ((c0 ∪ (b1 ∩ (a0a1))) ∪ (c1 ∪ (a0 ∩ (b0b1)))) = ((((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) ∪ (((a0a2) ∩ (b0b2)) ∪ (a0 ∩ (b0b1))))
9589, 94tr 62 . . . . . 6 ((c0c1) ∪ ((b1 ∩ (a0a1)) ∪ (a0 ∩ (b0b1)))) = ((((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) ∪ (((a0a2) ∩ (b0b2)) ∪ (a0 ∩ (b0b1))))
96 leao1 162 . . . . . . . 8 (b1 ∩ (a0a1)) ≤ (b1b2)
9796mli 1126 . . . . . . 7 (((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) = ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1))))
98 leao1 162 . . . . . . . 8 (a0 ∩ (b0b1)) ≤ (a0a2)
9998mli 1126 . . . . . . 7 (((a0a2) ∩ (b0b2)) ∪ (a0 ∩ (b0b1))) = ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1))))
10097, 992or 72 . . . . . 6 ((((b1b2) ∩ (a1a2)) ∪ (b1 ∩ (a0a1))) ∪ (((a0a2) ∩ (b0b2)) ∪ (a0 ∩ (b0b1)))) = (((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1)))))
10188, 95, 1003tr 65 . . . . 5 ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))) = (((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1)))))
102 or32 82 . . . . . . . 8 ((a1a2) ∪ (b1 ∩ (a0a1))) = ((a1 ∪ (b1 ∩ (a0a1))) ∪ a2)
103 ml3 1130 . . . . . . . . . 10 (a1 ∪ (b1 ∩ (a0a1))) = (a1 ∪ (a0 ∩ (b1a1)))
104 orcom 73 . . . . . . . . . . . 12 (b1a1) = (a1b1)
105104lan 77 . . . . . . . . . . 11 (a0 ∩ (b1a1)) = (a0 ∩ (a1b1))
106105lor 70 . . . . . . . . . 10 (a1 ∪ (a0 ∩ (b1a1))) = (a1 ∪ (a0 ∩ (a1b1)))
107103, 106tr 62 . . . . . . . . 9 (a1 ∪ (b1 ∩ (a0a1))) = (a1 ∪ (a0 ∩ (a1b1)))
108107ror 71 . . . . . . . 8 ((a1 ∪ (b1 ∩ (a0a1))) ∪ a2) = ((a1 ∪ (a0 ∩ (a1b1))) ∪ a2)
109 or32 82 . . . . . . . 8 ((a1 ∪ (a0 ∩ (a1b1))) ∪ a2) = ((a1a2) ∪ (a0 ∩ (a1b1)))
110102, 108, 1093tr 65 . . . . . . 7 ((a1a2) ∪ (b1 ∩ (a0a1))) = ((a1a2) ∪ (a0 ∩ (a1b1)))
111110lan 77 . . . . . 6 ((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) = ((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1))))
112 or32 82 . . . . . . . 8 ((b0b2) ∪ (a0 ∩ (b0b1))) = ((b0 ∪ (a0 ∩ (b0b1))) ∪ b2)
113 orcom 73 . . . . . . . . . . . 12 (b0b1) = (b1b0)
114113lan 77 . . . . . . . . . . 11 (a0 ∩ (b0b1)) = (a0 ∩ (b1b0))
115114lor 70 . . . . . . . . . 10 (b0 ∪ (a0 ∩ (b0b1))) = (b0 ∪ (a0 ∩ (b1b0)))
116 ml3 1130 . . . . . . . . . 10 (b0 ∪ (a0 ∩ (b1b0))) = (b0 ∪ (b1 ∩ (a0b0)))
117115, 116tr 62 . . . . . . . . 9 (b0 ∪ (a0 ∩ (b0b1))) = (b0 ∪ (b1 ∩ (a0b0)))
118117ror 71 . . . . . . . 8 ((b0 ∪ (a0 ∩ (b0b1))) ∪ b2) = ((b0 ∪ (b1 ∩ (a0b0))) ∪ b2)
119 or32 82 . . . . . . . 8 ((b0 ∪ (b1 ∩ (a0b0))) ∪ b2) = ((b0b2) ∪ (b1 ∩ (a0b0)))
120112, 118, 1193tr 65 . . . . . . 7 ((b0b2) ∪ (a0 ∩ (b0b1))) = ((b0b2) ∪ (b1 ∩ (a0b0)))
121120lan 77 . . . . . 6 ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1)))) = ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0))))
122111, 1212or 72 . . . . 5 (((b1b2) ∩ ((a1a2) ∪ (b1 ∩ (a0a1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a0 ∩ (b0b1))))) = (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0)))))
123101, 122tr 62 . . . 4 ((c0c1) ∪ ((a0 ∩ (b0b1)) ∪ (b1 ∩ (a0a1)))) = (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0)))))
12486, 123lbtr 139 . . 3 c2 ≤ (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0)))))
125 lea 160 . . . . . . 7 (a0 ∩ (a1b1)) ≤ a0
12625leran 153 . . . . . . . 8 (a0 ∩ (a1b1)) ≤ ((a0b0) ∩ (a1b1))
127126, 37letr 137 . . . . . . 7 (a0 ∩ (a1b1)) ≤ (a2b2)
128125, 127ler2an 173 . . . . . 6 (a0 ∩ (a1b1)) ≤ (a0 ∩ (a2b2))
129128lelor 166 . . . . 5 ((a1a2) ∪ (a0 ∩ (a1b1))) ≤ ((a1a2) ∪ (a0 ∩ (a2b2)))
130129lelan 167 . . . 4 ((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ≤ ((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2))))
131 lea 160 . . . . . . 7 (b1 ∩ (a0b0)) ≤ b1
132 lear 161 . . . . . . . . 9 (b1 ∩ (a0b0)) ≤ (a0b0)
133 leao3 164 . . . . . . . . 9 (b1 ∩ (a0b0)) ≤ (a1b1)
134132, 133ler2an 173 . . . . . . . 8 (b1 ∩ (a0b0)) ≤ ((a0b0) ∩ (a1b1))
135134, 37letr 137 . . . . . . 7 (b1 ∩ (a0b0)) ≤ (a2b2)
136131, 135ler2an 173 . . . . . 6 (b1 ∩ (a0b0)) ≤ (b1 ∩ (a2b2))
137136lelor 166 . . . . 5 ((b0b2) ∪ (b1 ∩ (a0b0))) ≤ ((b0b2) ∪ (b1 ∩ (a2b2)))
138137lelan 167 . . . 4 ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0)))) ≤ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2))))
139130, 138le2or 168 . . 3 (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a1b1)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a0b0))))) ≤ (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2)))))
140124, 139letr 137 . 2 c2 ≤ (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2)))))
141 ax-a2 31 . . . . . . . . . 10 (a2b2) = (b2a2)
142141lan 77 . . . . . . . . 9 (a0 ∩ (a2b2)) = (a0 ∩ (b2a2))
143142lor 70 . . . . . . . 8 (a2 ∪ (a0 ∩ (a2b2))) = (a2 ∪ (a0 ∩ (b2a2)))
144 ml3 1130 . . . . . . . 8 (a2 ∪ (a0 ∩ (b2a2))) = (a2 ∪ (b2 ∩ (a0a2)))
145143, 144tr 62 . . . . . . 7 (a2 ∪ (a0 ∩ (a2b2))) = (a2 ∪ (b2 ∩ (a0a2)))
146145lor 70 . . . . . 6 (a1 ∪ (a2 ∪ (a0 ∩ (a2b2)))) = (a1 ∪ (a2 ∪ (b2 ∩ (a0a2))))
147 orass 75 . . . . . 6 ((a1a2) ∪ (a0 ∩ (a2b2))) = (a1 ∪ (a2 ∪ (a0 ∩ (a2b2))))
148 orass 75 . . . . . 6 ((a1a2) ∪ (b2 ∩ (a0a2))) = (a1 ∪ (a2 ∪ (b2 ∩ (a0a2))))
149146, 147, 1483tr1 63 . . . . 5 ((a1a2) ∪ (a0 ∩ (a2b2))) = ((a1a2) ∪ (b2 ∩ (a0a2)))
150149lan 77 . . . 4 ((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) = ((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2))))
151 ml3 1130 . . . . . . 7 (b2 ∪ (b1 ∩ (a2b2))) = (b2 ∪ (a2 ∩ (b1b2)))
152151lor 70 . . . . . 6 (b0 ∪ (b2 ∪ (b1 ∩ (a2b2)))) = (b0 ∪ (b2 ∪ (a2 ∩ (b1b2))))
153 orass 75 . . . . . 6 ((b0b2) ∪ (b1 ∩ (a2b2))) = (b0 ∪ (b2 ∪ (b1 ∩ (a2b2))))
154 orass 75 . . . . . 6 ((b0b2) ∪ (a2 ∩ (b1b2))) = (b0 ∪ (b2 ∪ (a2 ∩ (b1b2))))
155152, 153, 1543tr1 63 . . . . 5 ((b0b2) ∪ (b1 ∩ (a2b2))) = ((b0b2) ∪ (a2 ∩ (b1b2)))
156155lan 77 . . . 4 ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2)))) = ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2))))
157150, 1562or 72 . . 3 (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2))))) = (((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2)))))
158 leao3 164 . . . . . 6 (b2 ∩ (a0a2)) ≤ (b1b2)
159158mldual2i 1127 . . . . 5 ((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) = (((b1b2) ∩ (a1a2)) ∪ (b2 ∩ (a0a2)))
16091ror 71 . . . . . 6 (c0 ∪ (b2 ∩ (a0a2))) = (((b1b2) ∩ (a1a2)) ∪ (b2 ∩ (a0a2)))
161160cm 61 . . . . 5 (((b1b2) ∩ (a1a2)) ∪ (b2 ∩ (a0a2))) = (c0 ∪ (b2 ∩ (a0a2)))
162159, 161tr 62 . . . 4 ((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) = (c0 ∪ (b2 ∩ (a0a2)))
163 leao3 164 . . . . . 6 (a2 ∩ (b1b2)) ≤ (a0a2)
164163mldual2i 1127 . . . . 5 ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2)))) = (((a0a2) ∩ (b0b2)) ∪ (a2 ∩ (b1b2)))
16544ror 71 . . . . . 6 (c1 ∪ (a2 ∩ (b1b2))) = (((a0a2) ∩ (b0b2)) ∪ (a2 ∩ (b1b2)))
166165cm 61 . . . . 5 (((a0a2) ∩ (b0b2)) ∪ (a2 ∩ (b1b2))) = (c1 ∪ (a2 ∩ (b1b2)))
167164, 166tr 62 . . . 4 ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2)))) = (c1 ∪ (a2 ∩ (b1b2)))
168162, 1672or 72 . . 3 (((b1b2) ∩ ((a1a2) ∪ (b2 ∩ (a0a2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (a2 ∩ (b1b2))))) = ((c0 ∪ (b2 ∩ (a0a2))) ∪ (c1 ∪ (a2 ∩ (b1b2))))
169 or4 84 . . . 4 ((c0 ∪ (b2 ∩ (a0a2))) ∪ (c1 ∪ (a2 ∩ (b1b2)))) = ((c0c1) ∪ ((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2))))
170 orcom 73 . . . 4 ((c0c1) ∪ ((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2)))) = (((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2))) ∪ (c0c1))
171 ancom 74 . . . . . . . 8 (b2 ∩ (a0a2)) = ((a0a2) ∩ b2)
172 leor 159 . . . . . . . . 9 b2 ≤ (b0b2)
173172lelan 167 . . . . . . . 8 ((a0a2) ∩ b2) ≤ ((a0a2) ∩ (b0b2))
174171, 173bltr 138 . . . . . . 7 (b2 ∩ (a0a2)) ≤ ((a0a2) ∩ (b0b2))
175 leor 159 . . . . . . . 8 a2 ≤ (a1a2)
176175leran 153 . . . . . . 7 (a2 ∩ (b1b2)) ≤ ((a1a2) ∩ (b1b2))
177174, 176le2or 168 . . . . . 6 ((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2))) ≤ (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))
17844, 432or 72 . . . . . . . 8 (c1c0) = (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))
179178cm 61 . . . . . . 7 (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2))) = (c1c0)
180 orcom 73 . . . . . . 7 (c1c0) = (c0c1)
181179, 180tr 62 . . . . . 6 (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2))) = (c0c1)
182177, 181lbtr 139 . . . . 5 ((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2))) ≤ (c0c1)
183182df-le2 131 . . . 4 (((b2 ∩ (a0a2)) ∪ (a2 ∩ (b1b2))) ∪ (c0c1)) = (c0c1)
184169, 170, 1833tr 65 . . 3 ((c0 ∪ (b2 ∩ (a0a2))) ∪ (c1 ∪ (a2 ∩ (b1b2)))) = (c0c1)
185157, 168, 1843tr 65 . 2 (((b1b2) ∩ ((a1a2) ∪ (a0 ∩ (a2b2)))) ∪ ((a0a2) ∩ ((b0b2) ∪ (b1 ∩ (a2b2))))) = (c0c1)
186140, 185lbtr 139 1 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