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

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

Proof of Theorem oa3-5lem
StepHypRef Expression
1 or12 80 . . . . . . 7 ((ac) ∪ (a ∪ (ac))) = (a ∪ ((ac) ∪ (ac)))
2 oridm 110 . . . . . . . 8 ((ac) ∪ (ac)) = (ac)
32lor 70 . . . . . . 7 (a ∪ ((ac) ∪ (ac))) = (a ∪ (ac))
41, 3ax-r2 36 . . . . . 6 ((ac) ∪ (a ∪ (ac))) = (a ∪ (ac))
5 an1 106 . . . . . . . 8 ((a1 c) ∩ 1) = (a1 c)
6 df-i1 44 . . . . . . . 8 (a1 c) = (a ∪ (ac))
75, 6ax-r2 36 . . . . . . 7 ((a1 c) ∩ 1) = (a ∪ (ac))
87lor 70 . . . . . 6 ((ac) ∪ ((a1 c) ∩ 1)) = ((ac) ∪ (a ∪ (ac)))
94, 8, 63tr1 63 . . . . 5 ((ac) ∪ ((a1 c) ∩ 1)) = (a1 c)
10 or12 80 . . . . . . . . 9 ((cb) ∪ (b ∪ (bc))) = (b ∪ ((cb) ∪ (bc)))
11 ancom 74 . . . . . . . . . . . 12 (cb) = (bc)
1211ax-r5 38 . . . . . . . . . . 11 ((cb) ∪ (bc)) = ((bc) ∪ (bc))
13 oridm 110 . . . . . . . . . . 11 ((bc) ∪ (bc)) = (bc)
1412, 13ax-r2 36 . . . . . . . . . 10 ((cb) ∪ (bc)) = (bc)
1514lor 70 . . . . . . . . 9 (b ∪ ((cb) ∪ (bc))) = (b ∪ (bc))
1610, 15ax-r2 36 . . . . . . . 8 ((cb) ∪ (b ∪ (bc))) = (b ∪ (bc))
17 ancom 74 . . . . . . . . . 10 (1 ∩ (b1 c)) = ((b1 c) ∩ 1)
18 an1 106 . . . . . . . . . 10 ((b1 c) ∩ 1) = (b1 c)
19 df-i1 44 . . . . . . . . . 10 (b1 c) = (b ∪ (bc))
2017, 18, 193tr 65 . . . . . . . . 9 (1 ∩ (b1 c)) = (b ∪ (bc))
2120lor 70 . . . . . . . 8 ((cb) ∪ (1 ∩ (b1 c))) = ((cb) ∪ (b ∪ (bc)))
2216, 21, 193tr1 63 . . . . . . 7 ((cb) ∪ (1 ∩ (b1 c))) = (b1 c)
2322lan 77 . . . . . 6 (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))) = (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ (b1 c))
24 ancom 74 . . . . . 6 (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ (b1 c)) = ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))
2523, 24ax-r2 36 . . . . 5 (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))) = ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))
269, 252or 72 . . . 4 (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c))))) = ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))
2726lan 77 . . 3 (c ∩ (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))))) = (c ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))))
2827lor 70 . 2 (a ∪ (c ∩ (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c))))))) = (a ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))))))
2928lan 77 1 ((a1 c) ∩ (a ∪ (c ∩ (((ac) ∪ ((a1 c) ∩ 1)) ∪ (((ab) ∪ ((a1 c) ∩ (b1 c))) ∩ ((cb) ∪ (1 ∩ (b1 c)))))))) = ((a1 c) ∩ (a ∪ (c ∩ ((a1 c) ∪ ((b1 c) ∩ ((ab) ∪ ((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-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  df-i1 44
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator