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

Theorem u3lem13a 789
Description: Lemma for unified implication study. (Contributed by NM, 18-Jan-1998.)
Assertion
Ref Expression
u3lem13a (a3 (a3 b ) ) = (a1 b)

Proof of Theorem u3lem13a
StepHypRef Expression
1 df-i3 46 . 2 (a3 (a3 b ) ) = (((a ∩ (a3 b ) ) ∪ (a ∩ (a3 b ) )) ∪ (a ∩ (a ∪ (a3 b ) )))
2 ancom 74 . . . . . . 7 (a ∩ (a3 b ) ) = ((a3 b )a )
3 u3lemnana 647 . . . . . . 7 ((a3 b )a ) = (a ∩ ((ab ) ∩ (ab )))
42, 3ax-r2 36 . . . . . 6 (a ∩ (a3 b ) ) = (a ∩ ((ab ) ∩ (ab )))
5 ax-a1 30 . . . . . . . . 9 (a3 b ) = (a3 b )
65ax-r1 35 . . . . . . . 8 (a3 b ) = (a3 b )
76lan 77 . . . . . . 7 (a ∩ (a3 b ) ) = (a ∩ (a3 b ))
8 ancom 74 . . . . . . . 8 (a ∩ (a3 b )) = ((a3 b ) ∩ a )
9 u3lemana 607 . . . . . . . 8 ((a3 b ) ∩ a ) = ((ab ) ∪ (ab ))
108, 9ax-r2 36 . . . . . . 7 (a ∩ (a3 b )) = ((ab ) ∪ (ab ))
117, 10ax-r2 36 . . . . . 6 (a ∩ (a3 b ) ) = ((ab ) ∪ (ab ))
124, 112or 72 . . . . 5 ((a ∩ (a3 b ) ) ∪ (a ∩ (a3 b ) )) = ((a ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab )))
13 comanr1 464 . . . . . . . 8 a C (ab )
14 comanr1 464 . . . . . . . 8 a C (ab )
1513, 14com2or 483 . . . . . . 7 a C ((ab ) ∪ (ab ))
16 comorr 184 . . . . . . . . 9 a C (ab )
17 comorr 184 . . . . . . . . 9 a C (ab )
1816, 17com2an 484 . . . . . . . 8 a C ((ab ) ∩ (ab ))
1918comcom3 454 . . . . . . 7 a C ((ab ) ∩ (ab ))
2015, 19fh4r 476 . . . . . 6 ((a ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab ))) = ((a ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))))
21 ax-a2 31 . . . . . . . . 9 (a ∪ ((ab ) ∪ (ab ))) = (((ab ) ∪ (ab )) ∪ a )
22 lea 160 . . . . . . . . . . 11 (ab ) ≤ a
23 lea 160 . . . . . . . . . . 11 (ab ) ≤ a
2422, 23lel2or 170 . . . . . . . . . 10 ((ab ) ∪ (ab )) ≤ a
2524df-le2 131 . . . . . . . . 9 (((ab ) ∪ (ab )) ∪ a ) = a
2621, 25ax-r2 36 . . . . . . . 8 (a ∪ ((ab ) ∪ (ab ))) = a
27 anor2 89 . . . . . . . . . . . . 13 (ab ) = (ab )
28 anor3 90 . . . . . . . . . . . . 13 (ab ) = (ab )
2927, 282or 72 . . . . . . . . . . . 12 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ) )
30 ax-a2 31 . . . . . . . . . . . 12 ((ab ) ∪ (ab ) ) = ((ab ) ∪ (ab ) )
3129, 30ax-r2 36 . . . . . . . . . . 11 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ) )
32 oran3 93 . . . . . . . . . . 11 ((ab ) ∪ (ab ) ) = ((ab ) ∩ (ab ))
3331, 32ax-r2 36 . . . . . . . . . 10 ((ab ) ∪ (ab )) = ((ab ) ∩ (ab ))
3433lor 70 . . . . . . . . 9 (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))) = (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) )
35 df-t 41 . . . . . . . . . 10 1 = (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) )
3635ax-r1 35 . . . . . . . . 9 (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) ) = 1
3734, 36ax-r2 36 . . . . . . . 8 (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))) = 1
3826, 372an 79 . . . . . . 7 ((a ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab )))) = (a ∩ 1)
39 an1 106 . . . . . . 7 (a ∩ 1) = a
4038, 39ax-r2 36 . . . . . 6 ((a ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab )))) = a
4120, 40ax-r2 36 . . . . 5 ((a ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab ))) = a
4212, 41ax-r2 36 . . . 4 ((a ∩ (a3 b ) ) ∪ (a ∩ (a3 b ) )) = a
43 comid 187 . . . . . . 7 a C a
4443comcom2 183 . . . . . 6 a C a
45 comi31 508 . . . . . . 7 a C (a3 b )
4645comcom2 183 . . . . . 6 a C (a3 b )
4744, 46fh1 469 . . . . 5 (a ∩ (a ∪ (a3 b ) )) = ((aa ) ∪ (a ∩ (a3 b ) ))
48 dff 101 . . . . . . . 8 0 = (aa )
4948ax-r1 35 . . . . . . 7 (aa ) = 0
50 ancom 74 . . . . . . . 8 (a ∩ (a3 b ) ) = ((a3 b )a)
51 u3lemnaa 642 . . . . . . . 8 ((a3 b )a) = (ab )
5250, 51ax-r2 36 . . . . . . 7 (a ∩ (a3 b ) ) = (ab )
5349, 522or 72 . . . . . 6 ((aa ) ∪ (a ∩ (a3 b ) )) = (0 ∪ (ab ))
54 ax-a2 31 . . . . . . 7 (0 ∪ (ab )) = ((ab ) ∪ 0)
55 or0 102 . . . . . . 7 ((ab ) ∪ 0) = (ab )
5654, 55ax-r2 36 . . . . . 6 (0 ∪ (ab )) = (ab )
5753, 56ax-r2 36 . . . . 5 ((aa ) ∪ (a ∩ (a3 b ) )) = (ab )
5847, 57ax-r2 36 . . . 4 (a ∩ (a ∪ (a3 b ) )) = (ab )
5942, 582or 72 . . 3 (((a ∩ (a3 b ) ) ∪ (a ∩ (a3 b ) )) ∪ (a ∩ (a ∪ (a3 b ) ))) = (a ∪ (ab ))
60 ax-a1 30 . . . . . . 7 b = b
6160ax-r1 35 . . . . . 6 b = b
6261lan 77 . . . . 5 (ab ) = (ab)
6362lor 70 . . . 4 (a ∪ (ab )) = (a ∪ (ab))
64 df-i1 44 . . . . 5 (a1 b) = (a ∪ (ab))
6564ax-r1 35 . . . 4 (a ∪ (ab)) = (a1 b)
6663, 65ax-r2 36 . . 3 (a ∪ (ab )) = (a1 b)
6759, 66ax-r2 36 . 2 (((a ∩ (a3 b ) ) ∪ (a ∩ (a3 b ) )) ∪ (a ∩ (a ∪ (a3 b ) ))) = (a1 b)
681, 67ax-r2 36 1 (a3 (a3 b ) ) = (a1 b)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  0wf 9  1 wi1 12  3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  u3lem14aa2  793
  Copyright terms: Public domain W3C validator