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

Theorem oa3-u2lem 986
Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual. (Contributed by NM, 27-Dec-1998.)
Assertion
Ref Expression
oa3-u2lem ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))

Proof of Theorem oa3-u2lem
StepHypRef Expression
1 u1lemab 610 . . . . . . 7 ((a1 c) ∩ c) = ((ac) ∪ (a c))
2 an1 106 . . . . . . 7 ((a1 c) ∩ 1) = (a1 c)
31, 22or 72 . . . . . 6 (((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) = (((ac) ∪ (a c)) ∪ (a1 c))
4 lea 160 . . . . . . . . 9 (ac) ≤ a
5 ax-a1 30 . . . . . . . . . . . 12 a = a
65ax-r1 35 . . . . . . . . . . 11 a = a
7 leid 148 . . . . . . . . . . 11 aa
86, 7bltr 138 . . . . . . . . . 10 a a
98leran 153 . . . . . . . . 9 (a c) ≤ (ac)
104, 9le2or 168 . . . . . . . 8 ((ac) ∪ (a c)) ≤ (a ∪ (ac))
11 df-i1 44 . . . . . . . . 9 (a1 c) = (a ∪ (ac))
1211ax-r1 35 . . . . . . . 8 (a ∪ (ac)) = (a1 c)
1310, 12lbtr 139 . . . . . . 7 ((ac) ∪ (a c)) ≤ (a1 c)
1413df-le2 131 . . . . . 6 (((ac) ∪ (a c)) ∪ (a1 c)) = (a1 c)
153, 14ax-r2 36 . . . . 5 (((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) = (a1 c)
16 ancom 74 . . . . . 6 ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))) = (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))
17 ancom 74 . . . . . . . . . 10 (c ∩ (b1 c)) = ((b1 c) ∩ c)
18 u1lemab 610 . . . . . . . . . 10 ((b1 c) ∩ c) = ((bc) ∪ (b c))
1917, 18ax-r2 36 . . . . . . . . 9 (c ∩ (b1 c)) = ((bc) ∪ (b c))
20 ancom 74 . . . . . . . . . 10 (1 ∩ (b1 c)) = ((b1 c) ∩ 1)
21 an1 106 . . . . . . . . . 10 ((b1 c) ∩ 1) = (b1 c)
2220, 21ax-r2 36 . . . . . . . . 9 (1 ∩ (b1 c)) = (b1 c)
2319, 222or 72 . . . . . . . 8 ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) = (((bc) ∪ (b c)) ∪ (b1 c))
24 lea 160 . . . . . . . . . . 11 (bc) ≤ b
25 ax-a1 30 . . . . . . . . . . . . . 14 b = b
2625ax-r1 35 . . . . . . . . . . . . 13 b = b
27 leid 148 . . . . . . . . . . . . 13 bb
2826, 27bltr 138 . . . . . . . . . . . 12 b b
2928leran 153 . . . . . . . . . . 11 (b c) ≤ (bc)
3024, 29le2or 168 . . . . . . . . . 10 ((bc) ∪ (b c)) ≤ (b ∪ (bc))
31 df-i1 44 . . . . . . . . . . 11 (b1 c) = (b ∪ (bc))
3231ax-r1 35 . . . . . . . . . 10 (b ∪ (bc)) = (b1 c)
3330, 32lbtr 139 . . . . . . . . 9 ((bc) ∪ (b c)) ≤ (b1 c)
3433df-le2 131 . . . . . . . 8 (((bc) ∪ (b c)) ∪ (b1 c)) = (b1 c)
3523, 34ax-r2 36 . . . . . . 7 ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) = (b1 c)
36 ax-a2 31 . . . . . . 7 (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) = (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))
3735, 362an 79 . . . . . 6 (((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))) = ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))
3816, 37ax-r2 36 . . . . 5 ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))) = ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))
3915, 382or 72 . . . 4 ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))))) = ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))
4039lan 77 . . 3 (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))) = (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))
4140lor 70 . 2 ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c))))))) = ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))))))
4241lan 77 1 ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((((a1 c) ∩ c) ∪ ((a1 c) ∩ 1)) ∪ ((((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))) ∩ ((c ∩ (b1 c)) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ ((a1 c) ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c))))))))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  1 wi1 12
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  oa3-u2  992
  Copyright terms: Public domain W3C validator