QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud4lem1c Unicode version
Theorem ud4lem1c 579
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud4lem1c ((a ->4 b)' v (b ->4 a)) = (a v b')
Proof of Theorem ud4lem1c
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, 22or 72 . 2 ((a ->4 b)' v (b ->4 a)) = ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
4 comor2 462 . . . . . . . . . . . 12 (a' v b') C b'
54comcom3 454 . . . . . . . . . . 11 (a' v b')' C b'
65comcom5 458 . . . . . . . . . 10 (a' v b') C b
7 comor1 461 . . . . . . . . . . . 12 (a' v b') C a'
87comcom3 454 . . . . . . . . . . 11 (a' v b')' C a'
98comcom5 458 . . . . . . . . . 10 (a' v b') C a
106, 9com2an 484 . . . . . . . . 9 (a' v b') C (b ^ a)
114, 9com2an 484 . . . . . . . . 9 (a' v b') C (b' ^ a)
1210, 11com2or 483 . . . . . . . 8 (a' v b') C ((b ^ a) v (b' ^ a))
1312comcom 453 . . . . . . 7 ((b ^ a) v (b' ^ a)) C (a' v b')
14 comor2 462 . . . . . . . . . . . 12 (a v b') C b'
1514comcom3 454 . . . . . . . . . . 11 (a v b')' C b'
1615comcom5 458 . . . . . . . . . 10 (a v b') C b
17 comor1 461 . . . . . . . . . 10 (a v b') C a
1816, 17com2an 484 . . . . . . . . 9 (a v b') C (b ^ a)
1914, 17com2an 484 . . . . . . . . 9 (a v b') C (b' ^ a)
2018, 19com2or 483 . . . . . . . 8 (a v b') C ((b ^ a) v (b' ^ a))
2120comcom 453 . . . . . . 7 ((b ^ a) v (b' ^ a)) C (a v b')
2213, 21com2an 484 . . . . . 6 ((b ^ a) v (b' ^ a)) C ((a' v b') ^ (a v b'))
2322comcom 453 . . . . 5 ((a' v b') ^ (a v b')) C ((b ^ a) v (b' ^ a))
24 comor2 462 . . . . . . . . . 10 (b' v a) C a
2524comcom2 183 . . . . . . . . 9 (b' v a) C a'
26 comor1 461 . . . . . . . . 9 (b' v a) C b'
2725, 26com2or 483 . . . . . . . 8 (b' v a) C (a' v b')
2825comcom3 454 . . . . . . . . . 10 (b' v a)' C a'
2928comcom5 458 . . . . . . . . 9 (b' v a) C a
3029, 26com2or 483 . . . . . . . 8 (b' v a) C (a v b')
3127, 30com2an 484 . . . . . . 7 (b' v a) C ((a' v b') ^ (a v b'))
3231comcom 453 . . . . . 6 ((a' v b') ^ (a v b')) C (b' v a)
33 comorr 184 . . . . . . . 8 a' C (a' v b')
34 comorr 184 . . . . . . . . 9 a C (a v b')
3534comcom3 454 . . . . . . . 8 a' C (a v b')
3633, 35com2an 484 . . . . . . 7 a' C ((a' v b') ^ (a v b'))
3736comcom 453 . . . . . 6 ((a' v b') ^ (a v b')) C a'
3832, 37com2an 484 . . . . 5 ((a' v b') ^ (a v b')) C ((b' v a) ^ a')
3923, 38com2or 483 . . . 4 ((a' v b') ^ (a v b')) C (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
40 coman1 185 . . . . . . . . 9 (a ^ b') C a
4140comcom2 183 . . . . . . . 8 (a ^ b') C a'
42 coman2 186 . . . . . . . 8 (a ^ b') C b'
4341, 42com2or 483 . . . . . . 7 (a ^ b') C (a' v b')
4440, 42com2or 483 . . . . . . 7 (a ^ b') C (a v b')
4543, 44com2an 484 . . . . . 6 (a ^ b') C ((a' v b') ^ (a v b'))
4645comcom 453 . . . . 5 ((a' v b') ^ (a v b')) C (a ^ b')
474comcom 453 . . . . . . . . 9 b' C (a' v b')
4814comcom 453 . . . . . . . . 9 b' C (a v b')
4947, 48com2an 484 . . . . . . . 8 b' C ((a' v b') ^ (a v b'))
5049comcom 453 . . . . . . 7 ((a' v b') ^ (a v b')) C b'
5150comcom3 454 . . . . . 6 ((a' v b') ^ (a v b'))' C b'
5251comcom5 458 . . . . 5 ((a' v b') ^ (a v b')) C b
5346, 52com2or 483 . . . 4 ((a' v b') ^ (a v b')) C ((a ^ b') v b)
5439, 53fh4r 476 . . 3 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = ((((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))))
55 coman2 186 . . . . . . . . . . . 12 (b ^ a) C a
5655comcom2 183 . . . . . . . . . . 11 (b ^ a) C a'
57 coman1 185 . . . . . . . . . . . 12 (b ^ a) C b
5857comcom2 183 . . . . . . . . . . 11 (b ^ a) C b'
5956, 58com2or 483 . . . . . . . . . 10 (b ^ a) C (a' v b')
6059comcom 453 . . . . . . . . 9 (a' v b') C (b ^ a)
61 coman2 186 . . . . . . . . . . . 12 (b' ^ a) C a
6261comcom2 183 . . . . . . . . . . 11 (b' ^ a) C a'
63 coman1 185 . . . . . . . . . . 11 (b' ^ a) C b'
6462, 63com2or 483 . . . . . . . . . 10 (b' ^ a) C (a' v b')
6564comcom 453 . . . . . . . . 9 (a' v b') C (b' ^ a)
6660, 65com2or 483 . . . . . . . 8 (a' v b') C ((b ^ a) v (b' ^ a))
6727comcom 453 . . . . . . . . 9 (a' v b') C (b' v a)
6867, 7com2an 484 . . . . . . . 8 (a' v b') C ((b' v a) ^ a')
6966, 68com2or 483 . . . . . . 7 (a' v b') C (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))
7017comcom2 183 . . . . . . . . 9 (a v b') C a'
7170, 14com2or 483 . . . . . . . 8 (a v b') C (a' v b')
7271comcom 453 . . . . . . 7 (a' v b') C (a v b')
7369, 72fh4r 476 . . . . . 6 (((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))))
74 ax-a2 31 . . . . . . . . . . 11 (((a' v b') v (b ^ a)) v (b' ^ a)) = ((b' ^ a) v ((a' v b') v (b ^ a)))
75 ax-a3 32 . . . . . . . . . . 11 (((a' v b') v (b ^ a)) v (b' ^ a)) = ((a' v b') v ((b ^ a) v (b' ^ a)))
76 ax-a2 31 . . . . . . . . . . . . . . 15 (a' v b') = (b' v a')
77 df-a 40 . . . . . . . . . . . . . . 15 (b ^ a) = (b' v a')'
7876, 772or 72 . . . . . . . . . . . . . 14 ((a' v b') v (b ^ a)) = ((b' v a') v (b' v a')')
79 df-t 41 . . . . . . . . . . . . . . 15 1 = ((b' v a') v (b' v a')')
8079ax-r1 35 . . . . . . . . . . . . . 14 ((b' v a') v (b' v a')') = 1
8178, 80ax-r2 36 . . . . . . . . . . . . 13 ((a' v b') v (b ^ a)) = 1
8281lor 70 . . . . . . . . . . . 12 ((b' ^ a) v ((a' v b') v (b ^ a))) = ((b' ^ a) v 1)
83 or1 104 . . . . . . . . . . . 12 ((b' ^ a) v 1) = 1
8482, 83ax-r2 36 . . . . . . . . . . 11 ((b' ^ a) v ((a' v b') v (b ^ a))) = 1
8574, 75, 843tr2 64 . . . . . . . . . 10 ((a' v b') v ((b ^ a) v (b' ^ a))) = 1
8685ax-r5 38 . . . . . . . . 9 (((a' v b') v ((b ^ a) v (b' ^ a))) v ((b' v a) ^ a')) = (1 v ((b' v a) ^ a'))
87 ax-a3 32 . . . . . . . . 9 (((a' v b') v ((b ^ a) v (b' ^ a))) v ((b' v a) ^ a')) = ((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))
88 ax-a2 31 . . . . . . . . . 10 (1 v ((b' v a) ^ a')) = (((b' v a) ^ a') v 1)
89 or1 104 . . . . . . . . . 10 (((b' v a) ^ a') v 1) = 1
9088, 89ax-r2 36 . . . . . . . . 9 (1 v ((b' v a) ^ a')) = 1
9186, 87, 903tr2 64 . . . . . . . 8 ((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = 1
92 ax-a2 31 . . . . . . . . 9 ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v (a v b'))
93 lear 161 . . . . . . . . . . . . 13 (b ^ a) =< a
94 lear 161 . . . . . . . . . . . . 13 (b' ^ a) =< a
9593, 94lel2or 170 . . . . . . . . . . . 12 ((b ^ a) v (b' ^ a)) =< a
96 leo 158 . . . . . . . . . . . 12 a =< (a v b')
9795, 96letr 137 . . . . . . . . . . 11 ((b ^ a) v (b' ^ a)) =< (a v b')
98 lea 160 . . . . . . . . . . . 12 ((b' v a) ^ a') =< (b' v a)
99 ax-a2 31 . . . . . . . . . . . 12 (b' v a) = (a v b')
10098, 99lbtr 139 . . . . . . . . . . 11 ((b' v a) ^ a') =< (a v b')
10197, 100lel2or 170 . . . . . . . . . 10 (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) =< (a v b')
102101df-le2 131 . . . . . . . . 9 ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v (a v b')) = (a v b')
10392, 102ax-r2 36 . . . . . . . 8 ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (a v b')
10491, 1032an 79 . . . . . . 7 (((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))) = (1 ^ (a v b'))
105 ancom 74 . . . . . . . 8 (1 ^ (a v b')) = ((a v b') ^ 1)
106 an1 106 . . . . . . . 8 ((a v b') ^ 1) = (a v b')
107105, 106ax-r2 36 . . . . . . 7 (1 ^ (a v b')) = (a v b')
108104, 107ax-r2 36 . . . . . 6 (((a' v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ ((a v b') v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))) = (a v b')
10973, 108ax-r2 36 . . . . 5 (((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (a v b')
110 ax-a2 31 . . . . . 6 (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v ((a ^ b') v b))
111 or32 82 . . . . . . . 8 ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v ((a ^ b') v b)) = ((((b ^ a) v (b' ^ a)) v ((a ^ b') v b)) v ((b' v a) ^ a'))
112 or4 84 . . . . . . . . . 10 (((b ^ a) v (b' ^ a)) v ((a ^ b') v b)) = (((b ^ a) v (a ^ b')) v ((b' ^ a) v b))
113112ax-r5 38 . . . . . . . . 9 ((((b ^ a) v (b' ^ a)) v ((a ^ b') v b)) v ((b' v a) ^ a')) = ((((b ^ a) v (a ^ b')) v ((b' ^ a) v b)) v ((b' v a) ^ a'))
114 ax-a3 32 . . . . . . . . . 10 ((((b ^ a) v (a ^ b')) v ((b' ^ a) v b)) v ((b' v a) ^ a')) = (((b ^ a) v (a ^ b')) v (((b' ^ a) v b) v ((b' v a) ^ a')))
11526comcom3 454 . . . . . . . . . . . . . . . 16 (b' v a)' C b'
116115comcom5 458 . . . . . . . . . . . . . . 15 (b' v a) C b
117116, 25fh4 472 . . . . . . . . . . . . . 14 (b v ((b' v a) ^ a')) = ((b v (b' v a)) ^ (b v a'))
118 df-t 41 . . . . . . . . . . . . . . . . . . 19 1 = (b v b')
119118ax-r1 35 . . . . . . . . . . . . . . . . . 18 (b v b') = 1
120119ax-r5 38 . . . . . . . . . . . . . . . . 17 ((b v b') v a) = (1 v a)
121 ax-a3 32 . . . . . . . . . . . . . . . . 17 ((b v b') v a) = (b v (b' v a))
122 ax-a2 31 . . . . . . . . . . . . . . . . . 18 (1 v a) = (a v 1)
123 or1 104 . . . . . . . . . . . . . . . . . 18 (a v 1) = 1
124122, 123ax-r2 36 . . . . . . . . . . . . . . . . 17 (1 v a) = 1
125120, 121, 1243tr2 64 . . . . . . . . . . . . . . . 16 (b v (b' v a)) = 1
126 anor2 89 . . . . . . . . . . . . . . . . . 18 (b' ^ a) = (b v a')'
127126con2 67 . . . . . . . . . . . . . . . . 17 (b' ^ a)' = (b v a')
128127ax-r1 35 . . . . . . . . . . . . . . . 16 (b v a') = (b' ^ a)'
129125, 1282an 79 . . . . . . . . . . . . . . 15 ((b v (b' v a)) ^ (b v a')) = (1 ^ (b' ^ a)')
130 ancom 74 . . . . . . . . . . . . . . . 16 (1 ^ (b' ^ a)') = ((b' ^ a)' ^ 1)
131 an1 106 . . . . . . . . . . . . . . . 16 ((b' ^ a)' ^ 1) = (b' ^ a)'
132130, 131ax-r2 36 . . . . . . . . . . . . . . 15 (1 ^ (b' ^ a)') = (b' ^ a)'
133129, 132ax-r2 36 . . . . . . . . . . . . . 14 ((b v (b' v a)) ^ (b v a')) = (b' ^ a)'
134117, 133ax-r2 36 . . . . . . . . . . . . 13 (b v ((b' v a) ^ a')) = (b' ^ a)'
135134lor 70 . . . . . . . . . . . 12 ((b' ^ a) v (b v ((b' v a) ^ a'))) = ((b' ^ a) v (b' ^ a)')
136 ax-a3 32 . . . . . . . . . . . 12 (((b' ^ a) v b) v ((b' v a) ^ a')) = ((b' ^ a) v (b v ((b' v a) ^ a')))
137 df-t 41 . . . . . . . . . . . 12 1 = ((b' ^ a) v (b' ^ a)')
138135, 136, 1373tr1 63 . . . . . . . . . . 11 (((b' ^ a) v b) v ((b' v a) ^ a')) = 1
139138lor 70 . . . . . . . . . 10 (((b ^ a) v (a ^ b')) v (((b' ^ a) v b) v ((b' v a) ^ a'))) = (((b ^ a) v (a ^ b')) v 1)
140114, 139ax-r2 36 . . . . . . . . 9 ((((b ^ a) v (a ^ b')) v ((b' ^ a) v b)) v ((b' v a) ^ a')) = (((b ^ a) v (a ^ b')) v 1)
141113, 140ax-r2 36 . . . . . . . 8 ((((b ^ a) v (b' ^ a)) v ((a ^ b') v b)) v ((b' v a) ^ a')) = (((b ^ a) v (a ^ b')) v 1)
142111, 141ax-r2 36 . . . . . . 7 ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v ((a ^ b') v b)) = (((b ^ a) v (a ^ b')) v 1)
143 or1 104 . . . . . . 7 (((b ^ a) v (a ^ b')) v 1) = 1
144142, 143ax-r2 36 . . . . . 6 ((((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')) v ((a ^ b') v b)) = 1
145110, 144ax-r2 36 . . . . 5 (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = 1
146109, 1452an 79 . . . 4 ((((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))) = ((a v b') ^ 1)
147146, 106ax-r2 36 . . 3 ((((a' v b') ^ (a v b')) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) ^ (((a ^ b') v b) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a')))) = (a v b')
14854, 147ax-r2 36 . 2 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) v (((b ^ a) v (b' ^ a)) v ((b' v a) ^ a'))) = (a v b')
1493, 148ax-r2 36 1 ((a ->4 b)' v (b ->4 a)) = (a v b')
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->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:  ud4lem1d  580
  Copyright terms: Public domain W3C validator