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

Theorem ud5lem3 594
Description: Lemma for unified disjunction. (Contributed by NM, 26-Nov-1997.)
Assertion
Ref Expression
ud5lem3 ((a5 b) →5 (a ∪ (ab))) = (ab)

Proof of Theorem ud5lem3
StepHypRef Expression
1 df-i5 48 . 2 ((a5 b) →5 (a ∪ (ab))) = ((((a5 b) ∩ (a ∪ (ab))) ∪ ((a5 b) ∩ (a ∪ (ab)))) ∪ ((a5 b) ∩ (a ∪ (ab)) ))
2 ud5lem3a 591 . . . . 5 ((a5 b) ∩ (a ∪ (ab))) = ((ab) ∪ (ab))
3 ud5lem3b 592 . . . . 5 ((a5 b) ∩ (a ∪ (ab))) = (a ∩ (ab ))
42, 32or 72 . . . 4 (((a5 b) ∩ (a ∪ (ab))) ∪ ((a5 b) ∩ (a ∪ (ab)))) = (((ab) ∪ (ab)) ∪ (a ∩ (ab )))
5 ud5lem3c 593 . . . 4 ((a5 b) ∩ (a ∪ (ab)) ) = (((ab) ∩ (ab )) ∩ a )
64, 52or 72 . . 3 ((((a5 b) ∩ (a ∪ (ab))) ∪ ((a5 b) ∩ (a ∪ (ab)))) ∪ ((a5 b) ∩ (a ∪ (ab)) )) = ((((ab) ∪ (ab)) ∪ (a ∩ (ab ))) ∪ (((ab) ∩ (ab )) ∩ a ))
7 ax-a3 32 . . . 4 ((((ab) ∪ (ab)) ∪ (a ∩ (ab ))) ∪ (((ab) ∩ (ab )) ∩ a )) = (((ab) ∪ (ab)) ∪ ((a ∩ (ab )) ∪ (((ab) ∩ (ab )) ∩ a )))
8 or4 84 . . . . 5 (((ab) ∪ (ab)) ∪ ((a ∩ (ab )) ∪ (((ab) ∩ (ab )) ∩ a ))) = (((ab) ∪ (a ∩ (ab ))) ∪ ((ab) ∪ (((ab) ∩ (ab )) ∩ a )))
9 comanr1 464 . . . . . . . . 9 a C (ab)
10 comorr 184 . . . . . . . . . 10 a C (ab )
1110comcom6 459 . . . . . . . . 9 a C (ab )
129, 11fh4 472 . . . . . . . 8 ((ab) ∪ (a ∩ (ab ))) = (((ab) ∪ a) ∩ ((ab) ∪ (ab )))
13 ax-a2 31 . . . . . . . . . . 11 ((ab) ∪ a) = (a ∪ (ab))
14 orabs 120 . . . . . . . . . . 11 (a ∪ (ab)) = a
1513, 14ax-r2 36 . . . . . . . . . 10 ((ab) ∪ a) = a
16 df-a 40 . . . . . . . . . . . . . 14 (ab) = (ab )
1716ax-r1 35 . . . . . . . . . . . . 13 (ab ) = (ab)
1817con3 68 . . . . . . . . . . . 12 (ab ) = (ab)
1918lor 70 . . . . . . . . . . 11 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
20 df-t 41 . . . . . . . . . . . 12 1 = ((ab) ∪ (ab) )
2120ax-r1 35 . . . . . . . . . . 11 ((ab) ∪ (ab) ) = 1
2219, 21ax-r2 36 . . . . . . . . . 10 ((ab) ∪ (ab )) = 1
2315, 222an 79 . . . . . . . . 9 (((ab) ∪ a) ∩ ((ab) ∪ (ab ))) = (a ∩ 1)
24 an1 106 . . . . . . . . 9 (a ∩ 1) = a
2523, 24ax-r2 36 . . . . . . . 8 (((ab) ∪ a) ∩ ((ab) ∪ (ab ))) = a
2612, 25ax-r2 36 . . . . . . 7 ((ab) ∪ (a ∩ (ab ))) = a
27 coman1 185 . . . . . . . . . . . 12 (ab) C a
2827comcom7 460 . . . . . . . . . . 11 (ab) C a
29 coman2 186 . . . . . . . . . . 11 (ab) C b
3028, 29com2or 483 . . . . . . . . . 10 (ab) C (ab)
3129comcom2 183 . . . . . . . . . . 11 (ab) C b
3228, 31com2or 483 . . . . . . . . . 10 (ab) C (ab )
3330, 32com2an 484 . . . . . . . . 9 (ab) C ((ab) ∩ (ab ))
3433, 27fh3 471 . . . . . . . 8 ((ab) ∪ (((ab) ∩ (ab )) ∩ a )) = (((ab) ∪ ((ab) ∩ (ab ))) ∩ ((ab) ∪ a ))
35 comor1 461 . . . . . . . . . . . . . 14 (ab) C a
3635comcom2 183 . . . . . . . . . . . . 13 (ab) C a
37 comor2 462 . . . . . . . . . . . . 13 (ab) C b
3836, 37com2an 484 . . . . . . . . . . . 12 (ab) C (ab)
3937comcom2 183 . . . . . . . . . . . . 13 (ab) C b
4035, 39com2or 483 . . . . . . . . . . . 12 (ab) C (ab )
4138, 40fh4 472 . . . . . . . . . . 11 ((ab) ∪ ((ab) ∩ (ab ))) = (((ab) ∪ (ab)) ∩ ((ab) ∪ (ab )))
4236, 37fh3r 475 . . . . . . . . . . . . . 14 ((ab) ∪ (ab)) = ((a ∪ (ab)) ∩ (b ∪ (ab)))
43 ax-a2 31 . . . . . . . . . . . . . . . 16 (a ∪ (ab)) = ((ab) ∪ a )
44 or12 80 . . . . . . . . . . . . . . . . 17 (b ∪ (ab)) = (a ∪ (bb))
45 oridm 110 . . . . . . . . . . . . . . . . . 18 (bb) = b
4645lor 70 . . . . . . . . . . . . . . . . 17 (a ∪ (bb)) = (ab)
4744, 46ax-r2 36 . . . . . . . . . . . . . . . 16 (b ∪ (ab)) = (ab)
4843, 472an 79 . . . . . . . . . . . . . . 15 ((a ∪ (ab)) ∩ (b ∪ (ab))) = (((ab) ∪ a ) ∩ (ab))
49 ancom 74 . . . . . . . . . . . . . . . 16 (((ab) ∪ a ) ∩ (ab)) = ((ab) ∩ ((ab) ∪ a ))
50 anabs 121 . . . . . . . . . . . . . . . 16 ((ab) ∩ ((ab) ∪ a )) = (ab)
5149, 50ax-r2 36 . . . . . . . . . . . . . . 15 (((ab) ∪ a ) ∩ (ab)) = (ab)
5248, 51ax-r2 36 . . . . . . . . . . . . . 14 ((a ∪ (ab)) ∩ (b ∪ (ab))) = (ab)
5342, 52ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∪ (ab)) = (ab)
54 anor2 89 . . . . . . . . . . . . . . . . 17 (ab) = (ab )
5554ax-r1 35 . . . . . . . . . . . . . . . 16 (ab ) = (ab)
5655con3 68 . . . . . . . . . . . . . . 15 (ab ) = (ab)
5756lor 70 . . . . . . . . . . . . . 14 ((ab) ∪ (ab )) = ((ab) ∪ (ab) )
58 df-t 41 . . . . . . . . . . . . . . 15 1 = ((ab) ∪ (ab) )
5958ax-r1 35 . . . . . . . . . . . . . 14 ((ab) ∪ (ab) ) = 1
6057, 59ax-r2 36 . . . . . . . . . . . . 13 ((ab) ∪ (ab )) = 1
6153, 602an 79 . . . . . . . . . . . 12 (((ab) ∪ (ab)) ∩ ((ab) ∪ (ab ))) = ((ab) ∩ 1)
62 an1 106 . . . . . . . . . . . 12 ((ab) ∩ 1) = (ab)
6361, 62ax-r2 36 . . . . . . . . . . 11 (((ab) ∪ (ab)) ∩ ((ab) ∪ (ab ))) = (ab)
6441, 63ax-r2 36 . . . . . . . . . 10 ((ab) ∪ ((ab) ∩ (ab ))) = (ab)
65 ax-a2 31 . . . . . . . . . . 11 ((ab) ∪ a ) = (a ∪ (ab))
66 orabs 120 . . . . . . . . . . 11 (a ∪ (ab)) = a
6765, 66ax-r2 36 . . . . . . . . . 10 ((ab) ∪ a ) = a
6864, 672an 79 . . . . . . . . 9 (((ab) ∪ ((ab) ∩ (ab ))) ∩ ((ab) ∪ a )) = ((ab) ∩ a )
69 ancom 74 . . . . . . . . 9 ((ab) ∩ a ) = (a ∩ (ab))
7068, 69ax-r2 36 . . . . . . . 8 (((ab) ∪ ((ab) ∩ (ab ))) ∩ ((ab) ∪ a )) = (a ∩ (ab))
7134, 70ax-r2 36 . . . . . . 7 ((ab) ∪ (((ab) ∩ (ab )) ∩ a )) = (a ∩ (ab))
7226, 712or 72 . . . . . 6 (((ab) ∪ (a ∩ (ab ))) ∪ ((ab) ∪ (((ab) ∩ (ab )) ∩ a ))) = (a ∪ (a ∩ (ab)))
73 oml 445 . . . . . 6 (a ∪ (a ∩ (ab))) = (ab)
7472, 73ax-r2 36 . . . . 5 (((ab) ∪ (a ∩ (ab ))) ∪ ((ab) ∪ (((ab) ∩ (ab )) ∩ a ))) = (ab)
758, 74ax-r2 36 . . . 4 (((ab) ∪ (ab)) ∪ ((a ∩ (ab )) ∪ (((ab) ∩ (ab )) ∩ a ))) = (ab)
767, 75ax-r2 36 . . 3 ((((ab) ∪ (ab)) ∪ (a ∩ (ab ))) ∪ (((ab) ∩ (ab )) ∩ a )) = (ab)
776, 76ax-r2 36 . 2 ((((a5 b) ∩ (a ∪ (ab))) ∪ ((a5 b) ∩ (a ∪ (ab)))) ∪ ((a5 b) ∩ (a ∪ (ab)) )) = (ab)
781, 77ax-r2 36 1 ((a5 b) →5 (a ∪ (ab))) = (ab)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  5 wi5 16
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-i5 48  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud5  599
  Copyright terms: Public domain W3C validator