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

Theorem oa3-1lem 982
 Description: Lemma for 3-OA(1). Equivalence with substitution into 6-OA dual. (Contributed by NM, 25-Dec-1998.)
Assertion
Ref Expression
oa3-1lem (1 ∩ (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))

Proof of Theorem oa3-1lem
StepHypRef Expression
1 ancom 74 . 2 (1 ∩ (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))) = ((0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))) ∩ 1)
2 an1 106 . 2 ((0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))) ∩ 1) = (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))
3 ax-a2 31 . . 3 (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))) = ((a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ∪ 0)
4 or0 102 . . 3 ((a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) ∪ 0) = (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
5 ancom 74 . . . . . . . . 9 (0 ∩ a) = (a ∩ 0)
6 an0 108 . . . . . . . . 9 (a ∩ 0) = 0
75, 6ax-r2 36 . . . . . . . 8 (0 ∩ a) = 0
8 ancom 74 . . . . . . . . 9 (1 ∩ (a1 c)) = ((a1 c) ∩ 1)
9 an1 106 . . . . . . . . 9 ((a1 c) ∩ 1) = (a1 c)
108, 9ax-r2 36 . . . . . . . 8 (1 ∩ (a1 c)) = (a1 c)
117, 102or 72 . . . . . . 7 ((0 ∩ a) ∪ (1 ∩ (a1 c))) = (0 ∪ (a1 c))
12 ax-a2 31 . . . . . . 7 (0 ∪ (a1 c)) = ((a1 c) ∪ 0)
13 or0 102 . . . . . . 7 ((a1 c) ∪ 0) = (a1 c)
1411, 12, 133tr 65 . . . . . 6 ((0 ∩ a) ∪ (1 ∩ (a1 c))) = (a1 c)
1514ax-r5 38 . . . . 5 (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))) = ((a1 c) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))
16 ax-a2 31 . . . . . . . 8 ((0 ∩ b) ∪ (1 ∩ (b1 c))) = ((1 ∩ (b1 c)) ∪ (0 ∩ b))
17 ancom 74 . . . . . . . . . 10 (1 ∩ (b1 c)) = ((b1 c) ∩ 1)
18 an1 106 . . . . . . . . . 10 ((b1 c) ∩ 1) = (b1 c)
1917, 18ax-r2 36 . . . . . . . . 9 (1 ∩ (b1 c)) = (b1 c)
20 ancom 74 . . . . . . . . . 10 (0 ∩ b) = (b ∩ 0)
21 an0 108 . . . . . . . . . 10 (b ∩ 0) = 0
2220, 21ax-r2 36 . . . . . . . . 9 (0 ∩ b) = 0
2319, 222or 72 . . . . . . . 8 ((1 ∩ (b1 c)) ∪ (0 ∩ b)) = ((b1 c) ∪ 0)
24 or0 102 . . . . . . . 8 ((b1 c) ∪ 0) = (b1 c)
2516, 23, 243tr 65 . . . . . . 7 ((0 ∩ b) ∪ (1 ∩ (b1 c))) = (b1 c)
2625ran 78 . . . . . 6 (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) = ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))
2726lor 70 . . . . 5 ((a1 c) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))) = ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))
2815, 27ax-r2 36 . . . 4 (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))) = ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))
2928lan 77 . . 3 (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
303, 4, 293tr 65 . 2 (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
311, 2, 303tr 65 1 (1 ∩ (0 ∪ (a ∩ (((0 ∩ a) ∪ (1 ∩ (a1 c))) ∪ (((0 ∩ b) ∪ (1 ∩ (b1 c))) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))) = (a ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
 Colors of variables: term Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →1 wi1 12 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator