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

Theorem ud3lem3 576
Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
Assertion
Ref Expression
ud3lem3 ((a3 b) →3 (ab)) = (ab)

Proof of Theorem ud3lem3
StepHypRef Expression
1 df-i3 46 . 2 ((a3 b) →3 (ab)) = ((((a3 b) ∩ (ab)) ∪ ((a3 b) ∩ (ab) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (ab))))
2 ud3lem3a 572 . . . . . . 7 ((a3 b) ∩ (ab)) = (a3 b)
3 ud3lem0c 279 . . . . . . 7 (a3 b) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
42, 3ax-r2 36 . . . . . 6 ((a3 b) ∩ (ab)) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
5 ud3lem3b 573 . . . . . 6 ((a3 b) ∩ (ab) ) = 0
64, 52or 72 . . . . 5 (((a3 b) ∩ (ab)) ∪ ((a3 b) ∩ (ab) )) = ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ 0)
7 or0 102 . . . . 5 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ 0) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
86, 7ax-r2 36 . . . 4 (((a3 b) ∩ (ab)) ∪ ((a3 b) ∩ (ab) )) = (((ab ) ∩ (ab)) ∩ (a ∪ (ab )))
9 ud3lem3d 575 . . . 4 ((a3 b) ∩ ((a3 b) ∪ (ab))) = ((ab) ∪ (a ∩ (ab)))
108, 92or 72 . . 3 ((((a3 b) ∩ (ab)) ∪ ((a3 b) ∩ (ab) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (ab)))) = ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ ((ab) ∪ (a ∩ (ab))))
11 coman1 185 . . . . . . . . . 10 (ab) C a
1211comcom7 460 . . . . . . . . 9 (ab) C a
13 coman2 186 . . . . . . . . . 10 (ab) C b
1413comcom2 183 . . . . . . . . 9 (ab) C b
1512, 14com2or 483 . . . . . . . 8 (ab) C (ab )
1612, 13com2or 483 . . . . . . . 8 (ab) C (ab)
1715, 16com2an 484 . . . . . . 7 (ab) C ((ab ) ∩ (ab))
1817comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C (ab)
19 comorr 184 . . . . . . . . 9 a C (ab )
20 comorr 184 . . . . . . . . 9 a C (ab)
2119, 20com2an 484 . . . . . . . 8 a C ((ab ) ∩ (ab))
2221comcom 453 . . . . . . 7 ((ab ) ∩ (ab)) C a
23 comor1 461 . . . . . . . . . . 11 (ab) C a
2423comcom7 460 . . . . . . . . . 10 (ab) C a
25 comor2 462 . . . . . . . . . . 11 (ab) C b
2625comcom2 183 . . . . . . . . . 10 (ab) C b
2724, 26com2or 483 . . . . . . . . 9 (ab) C (ab )
2824, 25com2or 483 . . . . . . . . 9 (ab) C (ab)
2927, 28com2an 484 . . . . . . . 8 (ab) C ((ab ) ∩ (ab))
3029comcom 453 . . . . . . 7 ((ab ) ∩ (ab)) C (ab)
3122, 30com2an 484 . . . . . 6 ((ab ) ∩ (ab)) C (a ∩ (ab))
3218, 31com2or 483 . . . . 5 ((ab ) ∩ (ab)) C ((ab) ∪ (a ∩ (ab)))
3319comcom3 454 . . . . . . . 8 a C (ab )
3420comcom3 454 . . . . . . . 8 a C (ab)
3533, 34com2an 484 . . . . . . 7 a C ((ab ) ∩ (ab))
3635comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C a
37 coman1 185 . . . . . . . . 9 (ab ) C a
38 coman2 186 . . . . . . . . 9 (ab ) C b
3937, 38com2or 483 . . . . . . . 8 (ab ) C (ab )
4038comcom7 460 . . . . . . . . 9 (ab ) C b
4137, 40com2or 483 . . . . . . . 8 (ab ) C (ab)
4239, 41com2an 484 . . . . . . 7 (ab ) C ((ab ) ∩ (ab))
4342comcom 453 . . . . . 6 ((ab ) ∩ (ab)) C (ab )
4436, 43com2or 483 . . . . 5 ((ab ) ∩ (ab)) C (a ∪ (ab ))
4532, 44fh4r 476 . . . 4 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ ((ab) ∪ (a ∩ (ab)))) = ((((ab ) ∩ (ab)) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((a ∪ (ab )) ∪ ((ab) ∪ (a ∩ (ab)))))
46 comor1 461 . . . . . . . . . . 11 (ab ) C a
4746comcom2 183 . . . . . . . . . 10 (ab ) C a
48 comor2 462 . . . . . . . . . . 11 (ab ) C b
4948comcom7 460 . . . . . . . . . 10 (ab ) C b
5047, 49com2an 484 . . . . . . . . 9 (ab ) C (ab)
5147, 49com2or 483 . . . . . . . . . 10 (ab ) C (ab)
5246, 51com2an 484 . . . . . . . . 9 (ab ) C (a ∩ (ab))
5350, 52com2or 483 . . . . . . . 8 (ab ) C ((ab) ∪ (a ∩ (ab)))
5446, 49com2or 483 . . . . . . . 8 (ab ) C (ab)
5553, 54fh4r 476 . . . . . . 7 (((ab ) ∩ (ab)) ∪ ((ab) ∪ (a ∩ (ab)))) = (((ab ) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((ab) ∪ ((ab) ∪ (a ∩ (ab)))))
56 ax-a3 32 . . . . . . . . . . 11 (((ab ) ∪ (ab)) ∪ (a ∩ (ab))) = ((ab ) ∪ ((ab) ∪ (a ∩ (ab))))
5756ax-r1 35 . . . . . . . . . 10 ((ab ) ∪ ((ab) ∪ (a ∩ (ab)))) = (((ab ) ∪ (ab)) ∪ (a ∩ (ab)))
58 anor2 89 . . . . . . . . . . . . . 14 (ab) = (ab )
5958lor 70 . . . . . . . . . . . . 13 ((ab ) ∪ (ab)) = ((ab ) ∪ (ab ) )
60 df-t 41 . . . . . . . . . . . . . 14 1 = ((ab ) ∪ (ab ) )
6160ax-r1 35 . . . . . . . . . . . . 13 ((ab ) ∪ (ab ) ) = 1
6259, 61ax-r2 36 . . . . . . . . . . . 12 ((ab ) ∪ (ab)) = 1
6362ax-r5 38 . . . . . . . . . . 11 (((ab ) ∪ (ab)) ∪ (a ∩ (ab))) = (1 ∪ (a ∩ (ab)))
64 or1r 105 . . . . . . . . . . 11 (1 ∪ (a ∩ (ab))) = 1
6563, 64ax-r2 36 . . . . . . . . . 10 (((ab ) ∪ (ab)) ∪ (a ∩ (ab))) = 1
6657, 65ax-r2 36 . . . . . . . . 9 ((ab ) ∪ ((ab) ∪ (a ∩ (ab)))) = 1
67 ax-a2 31 . . . . . . . . . 10 ((ab) ∪ ((ab) ∪ (a ∩ (ab)))) = (((ab) ∪ (a ∩ (ab))) ∪ (ab))
68 lear 161 . . . . . . . . . . . . 13 (ab) ≤ b
69 leor 159 . . . . . . . . . . . . 13 b ≤ (ab)
7068, 69letr 137 . . . . . . . . . . . 12 (ab) ≤ (ab)
71 lea 160 . . . . . . . . . . . . 13 (a ∩ (ab)) ≤ a
72 leo 158 . . . . . . . . . . . . 13 a ≤ (ab)
7371, 72letr 137 . . . . . . . . . . . 12 (a ∩ (ab)) ≤ (ab)
7470, 73lel2or 170 . . . . . . . . . . 11 ((ab) ∪ (a ∩ (ab))) ≤ (ab)
7574df-le2 131 . . . . . . . . . 10 (((ab) ∪ (a ∩ (ab))) ∪ (ab)) = (ab)
7667, 75ax-r2 36 . . . . . . . . 9 ((ab) ∪ ((ab) ∪ (a ∩ (ab)))) = (ab)
7766, 762an 79 . . . . . . . 8 (((ab ) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((ab) ∪ ((ab) ∪ (a ∩ (ab))))) = (1 ∩ (ab))
78 an1r 107 . . . . . . . 8 (1 ∩ (ab)) = (ab)
7977, 78ax-r2 36 . . . . . . 7 (((ab ) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((ab) ∪ ((ab) ∪ (a ∩ (ab))))) = (ab)
8055, 79ax-r2 36 . . . . . 6 (((ab ) ∩ (ab)) ∪ ((ab) ∪ (a ∩ (ab)))) = (ab)
81 or12 80 . . . . . . 7 ((a ∪ (ab )) ∪ ((ab) ∪ (a ∩ (ab)))) = ((ab) ∪ ((a ∪ (ab )) ∪ (a ∩ (ab))))
82 df-a 40 . . . . . . . . . . . 12 (a ∩ (ab)) = (a ∪ (ab) )
83 anor1 88 . . . . . . . . . . . . . . 15 (ab ) = (ab)
8483ax-r1 35 . . . . . . . . . . . . . 14 (ab) = (ab )
8584lor 70 . . . . . . . . . . . . 13 (a ∪ (ab) ) = (a ∪ (ab ))
8685ax-r4 37 . . . . . . . . . . . 12 (a ∪ (ab) ) = (a ∪ (ab ))
8782, 86ax-r2 36 . . . . . . . . . . 11 (a ∩ (ab)) = (a ∪ (ab ))
8887lor 70 . . . . . . . . . 10 ((a ∪ (ab )) ∪ (a ∩ (ab))) = ((a ∪ (ab )) ∪ (a ∪ (ab )) )
89 df-t 41 . . . . . . . . . . 11 1 = ((a ∪ (ab )) ∪ (a ∪ (ab )) )
9089ax-r1 35 . . . . . . . . . 10 ((a ∪ (ab )) ∪ (a ∪ (ab )) ) = 1
9188, 90ax-r2 36 . . . . . . . . 9 ((a ∪ (ab )) ∪ (a ∩ (ab))) = 1
9291lor 70 . . . . . . . 8 ((ab) ∪ ((a ∪ (ab )) ∪ (a ∩ (ab)))) = ((ab) ∪ 1)
93 or1 104 . . . . . . . 8 ((ab) ∪ 1) = 1
9492, 93ax-r2 36 . . . . . . 7 ((ab) ∪ ((a ∪ (ab )) ∪ (a ∩ (ab)))) = 1
9581, 94ax-r2 36 . . . . . 6 ((a ∪ (ab )) ∪ ((ab) ∪ (a ∩ (ab)))) = 1
9680, 952an 79 . . . . 5 ((((ab ) ∩ (ab)) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((a ∪ (ab )) ∪ ((ab) ∪ (a ∩ (ab))))) = ((ab) ∩ 1)
97 an1 106 . . . . 5 ((ab) ∩ 1) = (ab)
9896, 97ax-r2 36 . . . 4 ((((ab ) ∩ (ab)) ∪ ((ab) ∪ (a ∩ (ab)))) ∩ ((a ∪ (ab )) ∪ ((ab) ∪ (a ∩ (ab))))) = (ab)
9945, 98ax-r2 36 . . 3 ((((ab ) ∩ (ab)) ∩ (a ∪ (ab ))) ∪ ((ab) ∪ (a ∩ (ab)))) = (ab)
10010, 99ax-r2 36 . 2 ((((a3 b) ∩ (ab)) ∪ ((a3 b) ∩ (ab) )) ∪ ((a3 b) ∩ ((a3 b) ∪ (ab)))) = (ab)
1011, 100ax-r2 36 1 ((a3 b) →3 (ab)) = (ab)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1wt 8  0wf 9  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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud3  597
  Copyright terms: Public domain W3C validator