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

Theorem ud5lem1b 587
Description: Lemma for unified disjunction. (Contributed by NM, 27-Nov-1997.)
Assertion
Ref Expression
ud5lem1b ((a5 b) ∩ (b5 a)) = (ab )

Proof of Theorem ud5lem1b
StepHypRef Expression
1 ud5lem0c 281 . . 3 (a5 b) = (((ab ) ∩ (ab )) ∩ (ab))
2 df-i5 48 . . . 4 (b5 a) = (((ba) ∪ (ba)) ∪ (ba ))
3 ax-a2 31 . . . 4 (((ba) ∪ (ba)) ∪ (ba )) = ((ba ) ∪ ((ba) ∪ (ba)))
42, 3ax-r2 36 . . 3 (b5 a) = ((ba ) ∪ ((ba) ∪ (ba)))
51, 42an 79 . 2 ((a5 b) ∩ (b5 a)) = ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba ) ∪ ((ba) ∪ (ba))))
6 coman2 186 . . . . . . 7 (ba ) C a
7 coman1 185 . . . . . . 7 (ba ) C b
86, 7com2or 483 . . . . . 6 (ba ) C (ab )
96comcom7 460 . . . . . . 7 (ba ) C a
109, 7com2or 483 . . . . . 6 (ba ) C (ab )
118, 10com2an 484 . . . . 5 (ba ) C ((ab ) ∩ (ab ))
127comcom7 460 . . . . . 6 (ba ) C b
139, 12com2or 483 . . . . 5 (ba ) C (ab)
1411, 13com2an 484 . . . 4 (ba ) C (((ab ) ∩ (ab )) ∩ (ab))
1512, 9com2an 484 . . . . 5 (ba ) C (ba)
167, 9com2an 484 . . . . 5 (ba ) C (ba)
1715, 16com2or 483 . . . 4 (ba ) C ((ba) ∪ (ba))
1814, 17fh2 470 . . 3 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba ) ∪ ((ba) ∪ (ba)))) = (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba )) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba) ∪ (ba))))
19 anass 76 . . . . . 6 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba )) = (((ab ) ∩ (ab )) ∩ ((ab) ∩ (ba )))
20 ax-a2 31 . . . . . . . . . 10 (ab) = (ba)
21 oran 87 . . . . . . . . . . . 12 (ba) = (ba )
2221ax-r1 35 . . . . . . . . . . 11 (ba ) = (ba)
2322con3 68 . . . . . . . . . 10 (ba ) = (ba)
2420, 232an 79 . . . . . . . . 9 ((ab) ∩ (ba )) = ((ba) ∩ (ba) )
25 dff 101 . . . . . . . . . 10 0 = ((ba) ∩ (ba) )
2625ax-r1 35 . . . . . . . . 9 ((ba) ∩ (ba) ) = 0
2724, 26ax-r2 36 . . . . . . . 8 ((ab) ∩ (ba )) = 0
2827lan 77 . . . . . . 7 (((ab ) ∩ (ab )) ∩ ((ab) ∩ (ba ))) = (((ab ) ∩ (ab )) ∩ 0)
29 an0 108 . . . . . . 7 (((ab ) ∩ (ab )) ∩ 0) = 0
3028, 29ax-r2 36 . . . . . 6 (((ab ) ∩ (ab )) ∩ ((ab) ∩ (ba ))) = 0
3119, 30ax-r2 36 . . . . 5 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba )) = 0
32 coman2 186 . . . . . . . . . . 11 (ba) C a
3332comcom2 183 . . . . . . . . . 10 (ba) C a
34 coman1 185 . . . . . . . . . . 11 (ba) C b
3534comcom2 183 . . . . . . . . . 10 (ba) C b
3633, 35com2or 483 . . . . . . . . 9 (ba) C (ab )
3732, 35com2or 483 . . . . . . . . 9 (ba) C (ab )
3836, 37com2an 484 . . . . . . . 8 (ba) C ((ab ) ∩ (ab ))
3932, 34com2or 483 . . . . . . . 8 (ba) C (ab)
4038, 39com2an 484 . . . . . . 7 (ba) C (((ab ) ∩ (ab )) ∩ (ab))
4135, 32com2an 484 . . . . . . 7 (ba) C (ba)
4240, 41fh2 470 . . . . . 6 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba) ∪ (ba))) = (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)))
43 an32 83 . . . . . . . . 9 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) = ((((ab ) ∩ (ab )) ∩ (ba)) ∩ (ab))
44 an32 83 . . . . . . . . . . . 12 (((ab ) ∩ (ab )) ∩ (ba)) = (((ab ) ∩ (ba)) ∩ (ab ))
45 ax-a2 31 . . . . . . . . . . . . . . . 16 (ab ) = (ba )
46 df-a 40 . . . . . . . . . . . . . . . 16 (ba) = (ba )
4745, 462an 79 . . . . . . . . . . . . . . 15 ((ab ) ∩ (ba)) = ((ba ) ∩ (ba ) )
48 dff 101 . . . . . . . . . . . . . . . 16 0 = ((ba ) ∩ (ba ) )
4948ax-r1 35 . . . . . . . . . . . . . . 15 ((ba ) ∩ (ba ) ) = 0
5047, 49ax-r2 36 . . . . . . . . . . . . . 14 ((ab ) ∩ (ba)) = 0
5150ran 78 . . . . . . . . . . . . 13 (((ab ) ∩ (ba)) ∩ (ab )) = (0 ∩ (ab ))
52 an0r 109 . . . . . . . . . . . . 13 (0 ∩ (ab )) = 0
5351, 52ax-r2 36 . . . . . . . . . . . 12 (((ab ) ∩ (ba)) ∩ (ab )) = 0
5444, 53ax-r2 36 . . . . . . . . . . 11 (((ab ) ∩ (ab )) ∩ (ba)) = 0
5554ran 78 . . . . . . . . . 10 ((((ab ) ∩ (ab )) ∩ (ba)) ∩ (ab)) = (0 ∩ (ab))
56 an0r 109 . . . . . . . . . 10 (0 ∩ (ab)) = 0
5755, 56ax-r2 36 . . . . . . . . 9 ((((ab ) ∩ (ab )) ∩ (ba)) ∩ (ab)) = 0
5843, 57ax-r2 36 . . . . . . . 8 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) = 0
59 lea 160 . . . . . . . . . . . 12 (ba) ≤ b
60 leor 159 . . . . . . . . . . . . 13 b ≤ (ab )
61 leor 159 . . . . . . . . . . . . 13 b ≤ (ab )
6260, 61ler2an 173 . . . . . . . . . . . 12 b ≤ ((ab ) ∩ (ab ))
6359, 62letr 137 . . . . . . . . . . 11 (ba) ≤ ((ab ) ∩ (ab ))
64 lear 161 . . . . . . . . . . . 12 (ba) ≤ a
65 leo 158 . . . . . . . . . . . 12 a ≤ (ab)
6664, 65letr 137 . . . . . . . . . . 11 (ba) ≤ (ab)
6763, 66ler2an 173 . . . . . . . . . 10 (ba) ≤ (((ab ) ∩ (ab )) ∩ (ab))
6867df2le2 136 . . . . . . . . 9 ((ba) ∩ (((ab ) ∩ (ab )) ∩ (ab))) = (ba)
69 ancom 74 . . . . . . . . 9 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) = ((ba) ∩ (((ab ) ∩ (ab )) ∩ (ab)))
70 ancom 74 . . . . . . . . 9 (ab ) = (ba)
7168, 69, 703tr1 63 . . . . . . . 8 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) = (ab )
7258, 712or 72 . . . . . . 7 (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba))) = (0 ∪ (ab ))
73 or0r 103 . . . . . . 7 (0 ∪ (ab )) = (ab )
7472, 73ax-r2 36 . . . . . 6 (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba)) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba))) = (ab )
7542, 74ax-r2 36 . . . . 5 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba) ∪ (ba))) = (ab )
7631, 752or 72 . . . 4 (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba )) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba) ∪ (ba)))) = (0 ∪ (ab ))
7776, 73ax-r2 36 . . 3 (((((ab ) ∩ (ab )) ∩ (ab)) ∩ (ba )) ∪ ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba) ∪ (ba)))) = (ab )
7818, 77ax-r2 36 . 2 ((((ab ) ∩ (ab )) ∩ (ab)) ∩ ((ba ) ∪ ((ba) ∪ (ba)))) = (ab )
795, 78ax-r2 36 1 ((a5 b) ∩ (b5 a)) = (ab )
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  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:  ud5lem1  589
  Copyright terms: Public domain W3C validator