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

Theorem lem3.3.4 1053
 Description: Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
Hypothesis
Ref Expression
lem3.3.4.1 (b2 a) = 1
Assertion
Ref Expression
lem3.3.4 (a2 (a5 b)) = (a5 b)

Proof of Theorem lem3.3.4
StepHypRef Expression
1 df-i2 45 . 2 (a2 (a5 b)) = ((a5 b) ∪ (a ∩ (a5 b) ))
2 df-id5 1047 . . . . . . 7 (a5 b) = ((ab) ∪ (ab ))
32ax-r4 37 . . . . . 6 (a5 b) = ((ab) ∪ (ab ))
43lan 77 . . . . 5 (a ∩ (a5 b) ) = (a ∩ ((ab) ∪ (ab )) )
5 anor3 90 . . . . . . . 8 ((ab) ∩ (ab ) ) = ((ab) ∪ (ab ))
65ax-r1 35 . . . . . . 7 ((ab) ∪ (ab )) = ((ab) ∩ (ab ) )
7 oran3 93 . . . . . . . . 9 (ab ) = (ab)
87ax-r1 35 . . . . . . . 8 (ab) = (ab )
9 oran 87 . . . . . . . . 9 (ab) = (ab )
109ax-r1 35 . . . . . . . 8 (ab ) = (ab)
118, 102an 79 . . . . . . 7 ((ab) ∩ (ab ) ) = ((ab ) ∩ (ab))
126, 11ax-r2 36 . . . . . 6 ((ab) ∪ (ab )) = ((ab ) ∩ (ab))
1312lan 77 . . . . 5 (a ∩ ((ab) ∪ (ab )) ) = (a ∩ ((ab ) ∩ (ab)))
14 anabs 121 . . . . . . 7 (a ∩ (ab )) = a
1514ran 78 . . . . . 6 ((a ∩ (ab )) ∩ (ab)) = (a ∩ (ab))
16 anass 76 . . . . . 6 ((a ∩ (ab )) ∩ (ab)) = (a ∩ ((ab ) ∩ (ab)))
17 lem3.3.4.1 . . . . . . . 8 (b2 a) = 1
1817ax-r4 37 . . . . . . 7 (b2 a) = 1
199con2 67 . . . . . . . . . . 11 (ab) = (ab )
20 ancom 74 . . . . . . . . . . 11 (ab ) = (ba )
2119, 20ax-r2 36 . . . . . . . . . 10 (ab) = (ba )
2221lor 70 . . . . . . . . 9 (a ∪ (ab) ) = (a ∪ (ba ))
23 oran1 91 . . . . . . . . . 10 (a ∪ (ab) ) = (a ∩ (ab))
2423ax-r1 35 . . . . . . . . 9 (a ∩ (ab)) = (a ∪ (ab) )
25 df-i2 45 . . . . . . . . 9 (b2 a) = (a ∪ (ba ))
2622, 24, 253tr1 63 . . . . . . . 8 (a ∩ (ab)) = (b2 a)
2726con3 68 . . . . . . 7 (a ∩ (ab)) = (b2 a)
28 df-f 42 . . . . . . 7 0 = 1
2918, 27, 283tr1 63 . . . . . 6 (a ∩ (ab)) = 0
3015, 16, 293tr2 64 . . . . 5 (a ∩ ((ab ) ∩ (ab))) = 0
314, 13, 303tr 65 . . . 4 (a ∩ (a5 b) ) = 0
3231lor 70 . . 3 ((a5 b) ∪ (a ∩ (a5 b) )) = ((a5 b) ∪ 0)
33 ax-a2 31 . . 3 ((a5 b) ∪ 0) = (0 ∪ (a5 b))
3432, 33ax-r2 36 . 2 ((a5 b) ∪ (a ∩ (a5 b) )) = (0 ∪ (a5 b))
35 or0r 103 . 2 (0 ∪ (a5 b)) = (a5 b)
361, 34, 353tr 65 1 (a2 (a5 b)) = (a5 b)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →2 wi2 13   ≡5 wid5 22 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-i2 45  df-id5 1047 This theorem is referenced by:  lem3.4.4  1077
 Copyright terms: Public domain W3C validator