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

Theorem u3lem13b 790
Description: Lemma for unified implication study. (Contributed by NM, 19-Jan-1998.)
Assertion
Ref Expression
u3lem13b ((a3 b ) →3 a ) = (a1 b)

Proof of Theorem u3lem13b
StepHypRef Expression
1 df-i3 46 . 2 ((a3 b ) →3 a ) = ((((a3 b )a ) ∪ ((a3 b )a )) ∪ ((a3 b ) ∩ ((a3 b )a )))
2 u3lemnana 647 . . . . . 6 ((a3 b )a ) = (a ∩ ((ab ) ∩ (ab )))
3 ax-a1 30 . . . . . . . . 9 a = a
43ax-r1 35 . . . . . . . 8 a = a
54lan 77 . . . . . . 7 ((a3 b )a ) = ((a3 b )a)
6 u3lemnaa 642 . . . . . . 7 ((a3 b )a) = (ab )
75, 6ax-r2 36 . . . . . 6 ((a3 b )a ) = (ab )
82, 72or 72 . . . . 5 (((a3 b )a ) ∪ ((a3 b )a )) = ((a ∩ ((ab ) ∩ (ab ))) ∪ (ab ))
9 comanr1 464 . . . . . . . 8 a C (ab )
109comcom3 454 . . . . . . 7 a C (ab )
11 comorr 184 . . . . . . . . 9 a C (ab )
12 comorr 184 . . . . . . . . 9 a C (ab )
1311, 12com2an 484 . . . . . . . 8 a C ((ab ) ∩ (ab ))
1413comcom3 454 . . . . . . 7 a C ((ab ) ∩ (ab ))
1510, 14fh4r 476 . . . . . 6 ((a ∩ ((ab ) ∩ (ab ))) ∪ (ab )) = ((a ∪ (ab )) ∩ (((ab ) ∩ (ab )) ∪ (ab )))
16 coman1 185 . . . . . . . . . 10 (ab ) C a
17 coman2 186 . . . . . . . . . . 11 (ab ) C b
1817comcom7 460 . . . . . . . . . 10 (ab ) C b
1916, 18com2or 483 . . . . . . . . 9 (ab ) C (ab )
2016, 17com2or 483 . . . . . . . . 9 (ab ) C (ab )
2119, 20fh3r 475 . . . . . . . 8 (((ab ) ∩ (ab )) ∪ (ab )) = (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab )))
2221lan 77 . . . . . . 7 ((a ∪ (ab )) ∩ (((ab ) ∩ (ab )) ∪ (ab ))) = ((a ∪ (ab )) ∩ (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab ))))
23 ax-a2 31 . . . . . . . . . . . 12 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ))
24 lea 160 . . . . . . . . . . . . . 14 (ab ) ≤ a
25 leo 158 . . . . . . . . . . . . . 14 a ≤ (ab )
2624, 25letr 137 . . . . . . . . . . . . 13 (ab ) ≤ (ab )
2726df-le2 131 . . . . . . . . . . . 12 ((ab ) ∪ (ab )) = (ab )
2823, 27ax-r2 36 . . . . . . . . . . 11 ((ab ) ∪ (ab )) = (ab )
29 ax-a2 31 . . . . . . . . . . . 12 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ))
30 leo 158 . . . . . . . . . . . . . 14 a ≤ (ab )
3124, 30letr 137 . . . . . . . . . . . . 13 (ab ) ≤ (ab )
3231df-le2 131 . . . . . . . . . . . 12 ((ab ) ∪ (ab )) = (ab )
3329, 32ax-r2 36 . . . . . . . . . . 11 ((ab ) ∪ (ab )) = (ab )
3428, 332an 79 . . . . . . . . . 10 (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab ))) = ((ab ) ∩ (ab ))
35 id 59 . . . . . . . . . 10 ((ab ) ∩ (ab )) = ((ab ) ∩ (ab ))
3634, 35ax-r2 36 . . . . . . . . 9 (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab ))) = ((ab ) ∩ (ab ))
3736lan 77 . . . . . . . 8 ((a ∪ (ab )) ∩ (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab )))) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
38 id 59 . . . . . . . 8 ((a ∪ (ab )) ∩ ((ab ) ∩ (ab ))) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
3937, 38ax-r2 36 . . . . . . 7 ((a ∪ (ab )) ∩ (((ab ) ∪ (ab )) ∩ ((ab ) ∪ (ab )))) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
4022, 39ax-r2 36 . . . . . 6 ((a ∪ (ab )) ∩ (((ab ) ∩ (ab )) ∪ (ab ))) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
4115, 40ax-r2 36 . . . . 5 ((a ∩ ((ab ) ∩ (ab ))) ∪ (ab )) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
428, 41ax-r2 36 . . . 4 (((a3 b )a ) ∪ ((a3 b )a )) = ((a ∪ (ab )) ∩ ((ab ) ∩ (ab )))
43 u3lemnona 667 . . . . . 6 ((a3 b )a ) = (a ∪ (ab ))
4443lan 77 . . . . 5 ((a3 b ) ∩ ((a3 b )a )) = ((a3 b ) ∩ (a ∪ (ab )))
45 comi31 508 . . . . . . . 8 a C (a3 b )
4645comcom3 454 . . . . . . 7 a C (a3 b )
4746, 10fh2 470 . . . . . 6 ((a3 b ) ∩ (a ∪ (ab ))) = (((a3 b ) ∩ a ) ∪ ((a3 b ) ∩ (ab )))
48 u3lemana 607 . . . . . . . 8 ((a3 b ) ∩ a ) = ((ab ) ∪ (ab ))
49 anandi 114 . . . . . . . . 9 ((a3 b ) ∩ (ab )) = (((a3 b ) ∩ a) ∩ ((a3 b ) ∩ b ))
50 u3lemaa 602 . . . . . . . . . . 11 ((a3 b ) ∩ a) = (a ∩ (ab ))
51 u3lemanb 617 . . . . . . . . . . 11 ((a3 b ) ∩ b ) = (ab )
5250, 512an 79 . . . . . . . . . 10 (((a3 b ) ∩ a) ∩ ((a3 b ) ∩ b )) = ((a ∩ (ab )) ∩ (ab ))
53 an4 86 . . . . . . . . . . 11 ((a ∩ (ab )) ∩ (ab )) = ((aa ) ∩ ((ab ) ∩ b ))
54 ancom 74 . . . . . . . . . . . 12 ((aa ) ∩ ((ab ) ∩ b )) = (((ab ) ∩ b ) ∩ (aa ))
55 dff 101 . . . . . . . . . . . . . . 15 0 = (aa )
5655ax-r1 35 . . . . . . . . . . . . . 14 (aa ) = 0
5756lan 77 . . . . . . . . . . . . 13 (((ab ) ∩ b ) ∩ (aa )) = (((ab ) ∩ b ) ∩ 0)
58 an0 108 . . . . . . . . . . . . 13 (((ab ) ∩ b ) ∩ 0) = 0
5957, 58ax-r2 36 . . . . . . . . . . . 12 (((ab ) ∩ b ) ∩ (aa )) = 0
6054, 59ax-r2 36 . . . . . . . . . . 11 ((aa ) ∩ ((ab ) ∩ b )) = 0
6153, 60ax-r2 36 . . . . . . . . . 10 ((a ∩ (ab )) ∩ (ab )) = 0
6252, 61ax-r2 36 . . . . . . . . 9 (((a3 b ) ∩ a) ∩ ((a3 b ) ∩ b )) = 0
6349, 62ax-r2 36 . . . . . . . 8 ((a3 b ) ∩ (ab )) = 0
6448, 632or 72 . . . . . . 7 (((a3 b ) ∩ a ) ∪ ((a3 b ) ∩ (ab ))) = (((ab ) ∪ (ab )) ∪ 0)
65 or0 102 . . . . . . 7 (((ab ) ∪ (ab )) ∪ 0) = ((ab ) ∪ (ab ))
6664, 65ax-r2 36 . . . . . 6 (((a3 b ) ∩ a ) ∪ ((a3 b ) ∩ (ab ))) = ((ab ) ∪ (ab ))
6747, 66ax-r2 36 . . . . 5 ((a3 b ) ∩ (a ∪ (ab ))) = ((ab ) ∪ (ab ))
6844, 67ax-r2 36 . . . 4 ((a3 b ) ∩ ((a3 b )a )) = ((ab ) ∪ (ab ))
6942, 682or 72 . . 3 ((((a3 b )a ) ∪ ((a3 b )a )) ∪ ((a3 b ) ∩ ((a3 b )a ))) = (((a ∪ (ab )) ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab )))
70 comanr1 464 . . . . . . . . 9 a C (ab )
71 comanr1 464 . . . . . . . . 9 a C (ab )
7270, 71com2or 483 . . . . . . . 8 a C ((ab ) ∪ (ab ))
7372comcom 453 . . . . . . 7 ((ab ) ∪ (ab )) C a
7473comcom7 460 . . . . . . . 8 ((ab ) ∪ (ab )) C a
75 comanr2 465 . . . . . . . . . . 11 b C (ab )
7675comcom3 454 . . . . . . . . . 10 b C (ab )
77 comanr2 465 . . . . . . . . . 10 b C (ab )
7876, 77com2or 483 . . . . . . . . 9 b C ((ab ) ∪ (ab ))
7978comcom 453 . . . . . . . 8 ((ab ) ∪ (ab )) C b
8074, 79com2an 484 . . . . . . 7 ((ab ) ∪ (ab )) C (ab )
8173, 80com2or 483 . . . . . 6 ((ab ) ∪ (ab )) C (a ∪ (ab ))
8281comcom 453 . . . . 5 (a ∪ (ab )) C ((ab ) ∪ (ab ))
8313comcom 453 . . . . . . . 8 ((ab ) ∩ (ab )) C a
8483comcom2 183 . . . . . . 7 ((ab ) ∩ (ab )) C a
85 comorr2 463 . . . . . . . . . . 11 b C (ab )
8685comcom3 454 . . . . . . . . . 10 b C (ab )
87 comorr2 463 . . . . . . . . . 10 b C (ab )
8886, 87com2an 484 . . . . . . . . 9 b C ((ab ) ∩ (ab ))
8988comcom 453 . . . . . . . 8 ((ab ) ∩ (ab )) C b
9083, 89com2an 484 . . . . . . 7 ((ab ) ∩ (ab )) C (ab )
9184, 90com2or 483 . . . . . 6 ((ab ) ∩ (ab )) C (a ∪ (ab ))
9291comcom 453 . . . . 5 (a ∪ (ab )) C ((ab ) ∩ (ab ))
9382, 92fh4r 476 . . . 4 (((a ∪ (ab )) ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab ))) = (((a ∪ (ab )) ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))))
94 ax-a2 31 . . . . . . 7 ((a ∪ (ab )) ∪ ((ab ) ∪ (ab ))) = (((ab ) ∪ (ab )) ∪ (a ∪ (ab )))
95 lea 160 . . . . . . . . . . 11 (ab ) ≤ a
96 lea 160 . . . . . . . . . . 11 (ab ) ≤ a
9795, 96lel2or 170 . . . . . . . . . 10 ((ab ) ∪ (ab )) ≤ a
98 leo 158 . . . . . . . . . 10 a ≤ (a ∪ (ab ))
9997, 98letr 137 . . . . . . . . 9 ((ab ) ∪ (ab )) ≤ (a ∪ (ab ))
10099df-le2 131 . . . . . . . 8 (((ab ) ∪ (ab )) ∪ (a ∪ (ab ))) = (a ∪ (ab ))
101 id 59 . . . . . . . 8 (a ∪ (ab )) = (a ∪ (ab ))
102100, 101ax-r2 36 . . . . . . 7 (((ab ) ∪ (ab )) ∪ (a ∪ (ab ))) = (a ∪ (ab ))
10394, 102ax-r2 36 . . . . . 6 ((a ∪ (ab )) ∪ ((ab ) ∪ (ab ))) = (a ∪ (ab ))
104 ax-a2 31 . . . . . . . . 9 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ))
105 anor3 90 . . . . . . . . . . 11 (ab ) = (ab )
106 anor2 89 . . . . . . . . . . 11 (ab ) = (ab )
107105, 1062or 72 . . . . . . . . . 10 ((ab ) ∪ (ab )) = ((ab ) ∪ (ab ) )
108 oran3 93 . . . . . . . . . 10 ((ab ) ∪ (ab ) ) = ((ab ) ∩ (ab ))
109107, 108ax-r2 36 . . . . . . . . 9 ((ab ) ∪ (ab )) = ((ab ) ∩ (ab ))
110104, 109ax-r2 36 . . . . . . . 8 ((ab ) ∪ (ab )) = ((ab ) ∩ (ab ))
111110lor 70 . . . . . . 7 (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))) = (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) )
112 df-t 41 . . . . . . . 8 1 = (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) )
113112ax-r1 35 . . . . . . 7 (((ab ) ∩ (ab )) ∪ ((ab ) ∩ (ab )) ) = 1
114111, 113ax-r2 36 . . . . . 6 (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab ))) = 1
115103, 1142an 79 . . . . 5 (((a ∪ (ab )) ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab )))) = ((a ∪ (ab )) ∩ 1)
116 an1 106 . . . . . 6 ((a ∪ (ab )) ∩ 1) = (a ∪ (ab ))
117 df-i1 44 . . . . . . . 8 (a1 b ) = (a ∪ (ab ))
118117ax-r1 35 . . . . . . 7 (a ∪ (ab )) = (a1 b )
119 ax-a1 30 . . . . . . . . 9 b = b
120119ax-r1 35 . . . . . . . 8 b = b
121120ud1lem0a 255 . . . . . . 7 (a1 b ) = (a1 b)
122118, 121ax-r2 36 . . . . . 6 (a ∪ (ab )) = (a1 b)
123116, 122ax-r2 36 . . . . 5 ((a ∪ (ab )) ∩ 1) = (a1 b)
124115, 123ax-r2 36 . . . 4 (((a ∪ (ab )) ∪ ((ab ) ∪ (ab ))) ∩ (((ab ) ∩ (ab )) ∪ ((ab ) ∪ (ab )))) = (a1 b)
12593, 124ax-r2 36 . . 3 (((a ∪ (ab )) ∩ ((ab ) ∩ (ab ))) ∪ ((ab ) ∪ (ab ))) = (a1 b)
12669, 125ax-r2 36 . 2 ((((a3 b )a ) ∪ ((a3 b )a )) ∪ ((a3 b ) ∩ ((a3 b )a ))) = (a1 b)
1271, 126ax-r2 36 1 ((a3 b ) →3 a ) = (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:  u3lem14a  791  u3lem14aa2  793
  Copyright terms: Public domain W3C validator