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