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

Theorem lem3.3.7i1e2 1061
Description: Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
Assertion
Ref Expression
lem3.3.7i1e2 (a1 (ab)) = ((ab) ≡1 a)

Proof of Theorem lem3.3.7i1e2
StepHypRef Expression
1 oran3 93 . . . . . 6 (ab ) = (ab)
21ax-r1 35 . . . . 5 (ab) = (ab )
32lor 70 . . . 4 (a ∪ (ab) ) = (a ∪ (ab ))
43ran 78 . . 3 ((a ∪ (ab) ) ∩ (a ∪ (a ∩ (ab)))) = ((a ∪ (ab )) ∩ (a ∪ (a ∩ (ab))))
5 ax-a3 32 . . . . 5 ((aa ) ∪ b ) = (a ∪ (ab ))
65ax-r1 35 . . . 4 (a ∪ (ab )) = ((aa ) ∪ b )
76ran 78 . . 3 ((a ∪ (ab )) ∩ (a ∪ (a ∩ (ab)))) = (((aa ) ∪ b ) ∩ (a ∪ (a ∩ (ab))))
8 df-t 41 . . . . . . 7 1 = (aa )
98ax-r1 35 . . . . . 6 (aa ) = 1
109ax-r5 38 . . . . 5 ((aa ) ∪ b ) = (1 ∪ b )
1110ran 78 . . . 4 (((aa ) ∪ b ) ∩ (a ∪ (a ∩ (ab)))) = ((1 ∪ b ) ∩ (a ∪ (a ∩ (ab))))
12 or1r 105 . . . . 5 (1 ∪ b ) = 1
1312ran 78 . . . 4 ((1 ∪ b ) ∩ (a ∪ (a ∩ (ab)))) = (1 ∩ (a ∪ (a ∩ (ab))))
14 an1r 107 . . . . 5 (1 ∩ (a ∪ (a ∩ (ab)))) = (a ∪ (a ∩ (ab)))
15 anass 76 . . . . . . 7 ((aa) ∩ b) = (a ∩ (ab))
1615ax-r1 35 . . . . . 6 (a ∩ (ab)) = ((aa) ∩ b)
1716lor 70 . . . . 5 (a ∪ (a ∩ (ab))) = (a ∪ ((aa) ∩ b))
18 anidm 111 . . . . . . . 8 (aa) = a
1918ran 78 . . . . . . 7 ((aa) ∩ b) = (ab)
2019lor 70 . . . . . 6 (a ∪ ((aa) ∩ b)) = (a ∪ (ab))
21 ax-a2 31 . . . . . . . . 9 (a ∪ (ab)) = ((ab) ∪ a )
22 an1 106 . . . . . . . . . 10 (((ab) ∪ a ) ∩ 1) = ((ab) ∪ a )
2322ax-r1 35 . . . . . . . . 9 ((ab) ∪ a ) = (((ab) ∪ a ) ∩ 1)
24 df-t 41 . . . . . . . . . 10 1 = ((ab) ∪ (ab) )
2524lan 77 . . . . . . . . 9 (((ab) ∪ a ) ∩ 1) = (((ab) ∪ a ) ∩ ((ab) ∪ (ab) ))
2621, 23, 253tr 65 . . . . . . . 8 (a ∪ (ab)) = (((ab) ∪ a ) ∩ ((ab) ∪ (ab) ))
27 ax-a2 31 . . . . . . . . 9 ((ab) ∪ (ab) ) = ((ab) ∪ (ab))
2827lan 77 . . . . . . . 8 (((ab) ∪ a ) ∩ ((ab) ∪ (ab) )) = (((ab) ∪ a ) ∩ ((ab) ∪ (ab)))
2918ax-r1 35 . . . . . . . . . . 11 a = (aa)
3029ran 78 . . . . . . . . . 10 (ab) = ((aa) ∩ b)
3130lor 70 . . . . . . . . 9 ((ab) ∪ (ab)) = ((ab) ∪ ((aa) ∩ b))
3231lan 77 . . . . . . . 8 (((ab) ∪ a ) ∩ ((ab) ∪ (ab))) = (((ab) ∪ a ) ∩ ((ab) ∪ ((aa) ∩ b)))
3326, 28, 323tr 65 . . . . . . 7 (a ∪ (ab)) = (((ab) ∪ a ) ∩ ((ab) ∪ ((aa) ∩ b)))
3415lor 70 . . . . . . . 8 ((ab) ∪ ((aa) ∩ b)) = ((ab) ∪ (a ∩ (ab)))
3534lan 77 . . . . . . 7 (((ab) ∪ a ) ∩ ((ab) ∪ ((aa) ∩ b))) = (((ab) ∪ a ) ∩ ((ab) ∪ (a ∩ (ab))))
36 ancom 74 . . . . . . . . . 10 (ab) = (ba)
3736lan 77 . . . . . . . . 9 (a ∩ (ab)) = (a ∩ (ba))
3837lor 70 . . . . . . . 8 ((ab) ∪ (a ∩ (ab))) = ((ab) ∪ (a ∩ (ba)))
3938lan 77 . . . . . . 7 (((ab) ∪ a ) ∩ ((ab) ∪ (a ∩ (ab)))) = (((ab) ∪ a ) ∩ ((ab) ∪ (a ∩ (ba))))
4033, 35, 393tr 65 . . . . . 6 (a ∪ (ab)) = (((ab) ∪ a ) ∩ ((ab) ∪ (a ∩ (ba))))
41 anass 76 . . . . . . . . 9 ((ab) ∩ a) = (a ∩ (ba))
4241ax-r1 35 . . . . . . . 8 (a ∩ (ba)) = ((ab) ∩ a)
4342lor 70 . . . . . . 7 ((ab) ∪ (a ∩ (ba))) = ((ab) ∪ ((ab) ∩ a))
4443lan 77 . . . . . 6 (((ab) ∪ a ) ∩ ((ab) ∪ (a ∩ (ba)))) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
4520, 40, 443tr 65 . . . . 5 (a ∪ ((aa) ∩ b)) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
4614, 17, 453tr 65 . . . 4 (1 ∩ (a ∪ (a ∩ (ab)))) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
4711, 13, 463tr 65 . . 3 (((aa ) ∪ b ) ∩ (a ∪ (a ∩ (ab)))) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
484, 7, 473tr 65 . 2 ((a ∪ (ab) ) ∩ (a ∪ (a ∩ (ab)))) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
49 df-id1 50 . 2 (a1 (ab)) = ((a ∪ (ab) ) ∩ (a ∪ (a ∩ (ab))))
50 df-id1 50 . 2 ((ab) ≡1 a) = (((ab) ∪ a ) ∩ ((ab) ∪ ((ab) ∩ a)))
5148, 49, 503tr1 63 1 (a1 (ab)) = ((ab) ≡1 a)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  1 wid1 18
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
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-id1 50
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator