QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud4lem1b Unicode version
Theorem ud4lem1b 578
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud4lem1b ((a ->4 b)' ^ (b ->4 a)) = (a ^ b')
Proof of Theorem ud4lem1b
StepHypRef Expression
1 ud4lem0c 280 . . 3 (a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
2 df-i4 47 . . 3 (b ->4 a) = (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
31, 22an 79 . 2 ((a ->4 b)' ^ (b ->4 a)) = ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
4 coman2 186 . . . . . . . . . . 11 (b ^ a) C a
54comcom2 183 . . . . . . . . . 10 (b ^ a) C a'
6 coman1 185 . . . . . . . . . . 11 (b ^ a) C b
76comcom2 183 . . . . . . . . . 10 (b ^ a) C b'
85, 7com2or 483 . . . . . . . . 9 (b ^ a) C (a' v b')
98comcom 453 . . . . . . . 8 (a' v b') C (b ^ a)
10 coman2 186 . . . . . . . . . . 11 (b' ^ a) C a
1110comcom2 183 . . . . . . . . . 10 (b' ^ a) C a'
12 coman1 185 . . . . . . . . . 10 (b' ^ a) C b'
1311, 12com2or 483 . . . . . . . . 9 (b' ^ a) C (a' v b')
1413comcom 453 . . . . . . . 8 (a' v b') C (b' ^ a)
159, 14com2or 483 . . . . . . 7 (a' v b') C ((b ^ a) v (b' ^ a))
1615comcom 453 . . . . . 6 ((b ^ a) v (b' ^ a)) C (a' v b')
174, 7com2or 483 . . . . . . . . 9 (b ^ a) C (a v b')
1817comcom 453 . . . . . . . 8 (a v b') C (b ^ a)
19 comor2 462 . . . . . . . . 9 (a v b') C b'
20 comor1 461 . . . . . . . . 9 (a v b') C a
2119, 20com2an 484 . . . . . . . 8 (a v b') C (b' ^ a)
2218, 21com2or 483 . . . . . . 7 (a v b') C ((b ^ a) v (b' ^ a))
2322comcom 453 . . . . . 6 ((b ^ a) v (b' ^ a)) C (a v b')
2416, 23com2an 484 . . . . 5 ((b ^ a) v (b' ^ a)) C ((a' v b') ^ (a v b'))
25 coman2 186 . . . . . . . . . . 11 (a ^ b') C b'
2625comcom3 454 . . . . . . . . . 10 (a ^ b')' C b'
2726comcom5 458 . . . . . . . . 9 (a ^ b') C b
28 coman1 185 . . . . . . . . 9 (a ^ b') C a
2927, 28com2an 484 . . . . . . . 8 (a ^ b') C (b ^ a)
3025, 28com2an 484 . . . . . . . 8 (a ^ b') C (b' ^ a)
3129, 30com2or 483 . . . . . . 7 (a ^ b') C ((b ^ a) v (b' ^ a))
3231comcom 453 . . . . . 6 ((b ^ a) v (b' ^ a)) C (a ^ b')
336comcom 453 . . . . . . . 8 b C (b ^ a)
3412comcom 453 . . . . . . . . . 10 b' C (b' ^ a)
3534comcom2 183 . . . . . . . . 9 b' C (b' ^ a)'
3635comcom5 458 . . . . . . . 8 b C (b' ^ a)
3733, 36com2or 483 . . . . . . 7 b C ((b ^ a) v (b' ^ a))
3837comcom 453 . . . . . 6 ((b ^ a) v (b' ^ a)) C b
3932, 38com2or 483 . . . . 5 ((b ^ a) v (b' ^ a)) C ((a ^ b') v b)
4024, 39com2an 484 . . . 4 ((b ^ a) v (b' ^ a)) C (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
41 comor1 461 . . . . . . . . . 10 (b' v a) C b'
4241comcom3 454 . . . . . . . . 9 (b' v a)' C b'
4342comcom5 458 . . . . . . . 8 (b' v a) C b
44 comor2 462 . . . . . . . 8 (b' v a) C a
4543, 44com2an 484 . . . . . . 7 (b' v a) C (b ^ a)
4641, 44com2an 484 . . . . . . 7 (b' v a) C (b' ^ a)
4745, 46com2or 483 . . . . . 6 (b' v a) C ((b ^ a) v (b' ^ a))
4847comcom 453 . . . . 5 ((b ^ a) v (b' ^ a)) C (b' v a)
494comcom 453 . . . . . . . 8 a C (b ^ a)
5010comcom 453 . . . . . . . 8 a C (b' ^ a)
5149, 50com2or 483 . . . . . . 7 a C ((b ^ a) v (b' ^ a))
5251comcom 453 . . . . . 6 ((b ^ a) v (b' ^ a)) C a
5352comcom2 183 . . . . 5 ((b ^ a) v (b' ^ a)) C a'
5448, 53com2an 484 . . . 4 ((b ^ a) v (b' ^ a)) C ((b' v a) ^ a')
5540, 54fh2 470 . . 3 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b ^ a) v (b' ^ a))) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b' v a) ^ a')))
568, 17com2an 484 . . . . . . . 8 (b ^ a) C ((a' v b') ^ (a v b'))
574, 7com2an 484 . . . . . . . . 9 (b ^ a) C (a ^ b')
5857, 6com2or 483 . . . . . . . 8 (b ^ a) C ((a ^ b') v b)
5956, 58com2an 484 . . . . . . 7 (b ^ a) C (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
607, 4com2an 484 . . . . . . 7 (b ^ a) C (b' ^ a)
6159, 60fh2 470 . . . . . 6 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b ^ a) v (b' ^ a))) = (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a)))
62 an32 83 . . . . . . . . . 10 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) = ((((a' v b') ^ (a v b')) ^ (b ^ a)) ^ ((a ^ b') v b))
63 an32 83 . . . . . . . . . . . . 13 (((a' v b') ^ (a v b')) ^ (b ^ a)) = (((a' v b') ^ (b ^ a)) ^ (a v b'))
64 ax-a2 31 . . . . . . . . . . . . . . . . 17 (a' v b') = (b' v a')
65 df-a 40 . . . . . . . . . . . . . . . . 17 (b ^ a) = (b' v a')'
6664, 652an 79 . . . . . . . . . . . . . . . 16 ((a' v b') ^ (b ^ a)) = ((b' v a') ^ (b' v a')')
67 dff 101 . . . . . . . . . . . . . . . . 17 0 = ((b' v a') ^ (b' v a')')
6867ax-r1 35 . . . . . . . . . . . . . . . 16 ((b' v a') ^ (b' v a')') = 0
6966, 68ax-r2 36 . . . . . . . . . . . . . . 15 ((a' v b') ^ (b ^ a)) = 0
7069ran 78 . . . . . . . . . . . . . 14 (((a' v b') ^ (b ^ a)) ^ (a v b')) = (0 ^ (a v b'))
71 ancom 74 . . . . . . . . . . . . . . 15 (0 ^ (a v b')) = ((a v b') ^ 0)
72 an0 108 . . . . . . . . . . . . . . 15 ((a v b') ^ 0) = 0
7371, 72ax-r2 36 . . . . . . . . . . . . . 14 (0 ^ (a v b')) = 0
7470, 73ax-r2 36 . . . . . . . . . . . . 13 (((a' v b') ^ (b ^ a)) ^ (a v b')) = 0
7563, 74ax-r2 36 . . . . . . . . . . . 12 (((a' v b') ^ (a v b')) ^ (b ^ a)) = 0
7675ran 78 . . . . . . . . . . 11 ((((a' v b') ^ (a v b')) ^ (b ^ a)) ^ ((a ^ b') v b)) = (0 ^ ((a ^ b') v b))
77 ancom 74 . . . . . . . . . . . 12 (0 ^ ((a ^ b') v b)) = (((a ^ b') v b) ^ 0)
78 an0 108 . . . . . . . . . . . 12 (((a ^ b') v b) ^ 0) = 0
7977, 78ax-r2 36 . . . . . . . . . . 11 (0 ^ ((a ^ b') v b)) = 0
8076, 79ax-r2 36 . . . . . . . . . 10 ((((a' v b') ^ (a v b')) ^ (b ^ a)) ^ ((a ^ b') v b)) = 0
8162, 80ax-r2 36 . . . . . . . . 9 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) = 0
82 lea 160 . . . . . . . . . . . . . 14 (b' ^ a) =< b'
83 leor 159 . . . . . . . . . . . . . 14 b' =< (a' v b')
8482, 83letr 137 . . . . . . . . . . . . 13 (b' ^ a) =< (a' v b')
85 lear 161 . . . . . . . . . . . . . 14 (b' ^ a) =< a
86 leo 158 . . . . . . . . . . . . . 14 a =< (a v b')
8785, 86letr 137 . . . . . . . . . . . . 13 (b' ^ a) =< (a v b')
8884, 87ler2an 173 . . . . . . . . . . . 12 (b' ^ a) =< ((a' v b') ^ (a v b'))
89 ancom 74 . . . . . . . . . . . . 13 (b' ^ a) = (a ^ b')
90 leo 158 . . . . . . . . . . . . 13 (a ^ b') =< ((a ^ b') v b)
9189, 90bltr 138 . . . . . . . . . . . 12 (b' ^ a) =< ((a ^ b') v b)
9288, 91ler2an 173 . . . . . . . . . . 11 (b' ^ a) =< (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
9392df2le2 136 . . . . . . . . . 10 ((b' ^ a) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))) = (b' ^ a)
94 ancom 74 . . . . . . . . . 10 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a)) = ((b' ^ a) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b)))
95 ancom 74 . . . . . . . . . 10 (a ^ b') = (b' ^ a)
9693, 94, 953tr1 63 . . . . . . . . 9 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a)) = (a ^ b')
9781, 962or 72 . . . . . . . 8 (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a))) = (0 v (a ^ b'))
98 ax-a2 31 . . . . . . . 8 (0 v (a ^ b')) = ((a ^ b') v 0)
9997, 98ax-r2 36 . . . . . . 7 (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a))) = ((a ^ b') v 0)
100 or0 102 . . . . . . 7 ((a ^ b') v 0) = (a ^ b')
10199, 100ax-r2 36 . . . . . 6 (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b ^ a)) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (b' ^ a))) = (a ^ b')
10261, 101ax-r2 36 . . . . 5 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b ^ a) v (b' ^ a))) = (a ^ b')
103 anass 76 . . . . . 6 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b' v a) ^ a')) = (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ ((b' v a) ^ a')))
10425, 28com2or 483 . . . . . . . . . . 11 (a ^ b') C (b' v a)
10528comcom2 183 . . . . . . . . . . 11 (a ^ b') C a'
106104, 105com2an 484 . . . . . . . . . 10 (a ^ b') C ((b' v a) ^ a')
107106, 27fh2r 474 . . . . . . . . 9 (((a ^ b') v b) ^ ((b' v a) ^ a')) = (((a ^ b') ^ ((b' v a) ^ a')) v (b ^ ((b' v a) ^ a')))
108 an12 81 . . . . . . . . . . . 12 ((a ^ b') ^ ((b' v a) ^ a')) = ((b' v a) ^ ((a ^ b') ^ a'))
109 an32 83 . . . . . . . . . . . . . . 15 ((a ^ b') ^ a') = ((a ^ a') ^ b')
110 ancom 74 . . . . . . . . . . . . . . . 16 ((a ^ a') ^ b') = (b' ^ (a ^ a'))
111 dff 101 . . . . . . . . . . . . . . . . . . 19 0 = (a ^ a')
112111ax-r1 35 . . . . . . . . . . . . . . . . . 18 (a ^ a') = 0
113112lan 77 . . . . . . . . . . . . . . . . 17 (b' ^ (a ^ a')) = (b' ^ 0)
114 an0 108 . . . . . . . . . . . . . . . . 17 (b' ^ 0) = 0
115113, 114ax-r2 36 . . . . . . . . . . . . . . . 16 (b' ^ (a ^ a')) = 0
116110, 115ax-r2 36 . . . . . . . . . . . . . . 15 ((a ^ a') ^ b') = 0
117109, 116ax-r2 36 . . . . . . . . . . . . . 14 ((a ^ b') ^ a') = 0
118117lan 77 . . . . . . . . . . . . 13 ((b' v a) ^ ((a ^ b') ^ a')) = ((b' v a) ^ 0)
119 an0 108 . . . . . . . . . . . . 13 ((b' v a) ^ 0) = 0
120118, 119ax-r2 36 . . . . . . . . . . . 12 ((b' v a) ^ ((a ^ b') ^ a')) = 0
121108, 120ax-r2 36 . . . . . . . . . . 11 ((a ^ b') ^ ((b' v a) ^ a')) = 0
122 anor1 88 . . . . . . . . . . . . 13 (b ^ a') = (b' v a)'
123122lan 77 . . . . . . . . . . . 12 ((b' v a) ^ (b ^ a')) = ((b' v a) ^ (b' v a)')
124 an12 81 . . . . . . . . . . . 12 (b ^ ((b' v a) ^ a')) = ((b' v a) ^ (b ^ a'))
125 dff 101 . . . . . . . . . . . 12 0 = ((b' v a) ^ (b' v a)')
126123, 124, 1253tr1 63 . . . . . . . . . . 11 (b ^ ((b' v a) ^ a')) = 0
127121, 1262or 72 . . . . . . . . . 10 (((a ^ b') ^ ((b' v a) ^ a')) v (b ^ ((b' v a) ^ a'))) = (0 v 0)
128 or0 102 . . . . . . . . . 10 (0 v 0) = 0
129127, 128ax-r2 36 . . . . . . . . 9 (((a ^ b') ^ ((b' v a) ^ a')) v (b ^ ((b' v a) ^ a'))) = 0
130107, 129ax-r2 36 . . . . . . . 8 (((a ^ b') v b) ^ ((b' v a) ^ a')) = 0
131130lan 77 . . . . . . 7 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ ((b' v a) ^ a'))) = (((a' v b') ^ (a v b')) ^ 0)
132 an0 108 . . . . . . 7 (((a' v b') ^ (a v b')) ^ 0) = 0
133131, 132ax-r2 36 . . . . . 6 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ ((b' v a) ^ a'))) = 0
134103, 133ax-r2 36 . . . . 5 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b' v a) ^ a')) = 0
135102, 1342or 72 . . . 4 (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b ^ a) v (b' ^ a))) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b' v a) ^ a'))) = ((a ^ b') v 0)
136135, 100ax-r2 36 . . 3 (((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b ^ a) v (b' ^ a))) v ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ ((b' v a) ^ a'))) = (a ^ b')
13755, 136ax-r2 36 . 2 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (a ^ b')
1383, 137ax-r2 36 1 ((a ->4 b)' ^ (b ->4 a)) = (a ^ b')
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  0wf 9   ->4 wi4 15
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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud4lem1  581
  Copyright terms: Public domain W3C validator