QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud3lem1a Unicode version
Theorem ud3lem1a 566
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud3lem1a ((a ->3 b)' ^ (b ->3 a)) = (a ^ b')
Proof of Theorem ud3lem1a
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
2 df-i3 46 . . 3 (b ->3 a) = (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))
31, 22an 79 . 2 ((a ->3 b)' ^ (b ->3 a)) = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a))))
4 comor2 462 . . . . . . . . 9 (a v b') C b'
5 comor1 461 . . . . . . . . 9 (a v b') C a
64, 5com2an 484 . . . . . . . 8 (a v b') C (b' ^ a)
75comcom2 183 . . . . . . . . 9 (a v b') C a'
84, 7com2an 484 . . . . . . . 8 (a v b') C (b' ^ a')
96, 8com2or 483 . . . . . . 7 (a v b') C ((b' ^ a) v (b' ^ a'))
109comcom 453 . . . . . 6 ((b' ^ a) v (b' ^ a')) C (a v b')
11 comor2 462 . . . . . . . . . 10 (a v b) C b
1211comcom2 183 . . . . . . . . 9 (a v b) C b'
13 comor1 461 . . . . . . . . 9 (a v b) C a
1412, 13com2an 484 . . . . . . . 8 (a v b) C (b' ^ a)
1513comcom2 183 . . . . . . . . 9 (a v b) C a'
1612, 15com2an 484 . . . . . . . 8 (a v b) C (b' ^ a')
1714, 16com2or 483 . . . . . . 7 (a v b) C ((b' ^ a) v (b' ^ a'))
1817comcom 453 . . . . . 6 ((b' ^ a) v (b' ^ a')) C (a v b)
1910, 18com2an 484 . . . . 5 ((b' ^ a) v (b' ^ a')) C ((a v b') ^ (a v b))
20 comanr2 465 . . . . . . . . 9 a C (b' ^ a)
2120comcom3 454 . . . . . . . 8 a' C (b' ^ a)
22 comanr2 465 . . . . . . . 8 a' C (b' ^ a')
2321, 22com2or 483 . . . . . . 7 a' C ((b' ^ a) v (b' ^ a'))
2423comcom 453 . . . . . 6 ((b' ^ a) v (b' ^ a')) C a'
25 coman2 186 . . . . . . . . 9 (a ^ b') C b'
26 coman1 185 . . . . . . . . 9 (a ^ b') C a
2725, 26com2an 484 . . . . . . . 8 (a ^ b') C (b' ^ a)
2826comcom2 183 . . . . . . . . 9 (a ^ b') C a'
2925, 28com2an 484 . . . . . . . 8 (a ^ b') C (b' ^ a')
3027, 29com2or 483 . . . . . . 7 (a ^ b') C ((b' ^ a) v (b' ^ a'))
3130comcom 453 . . . . . 6 ((b' ^ a) v (b' ^ a')) C (a ^ b')
3224, 31com2or 483 . . . . 5 ((b' ^ a) v (b' ^ a')) C (a' v (a ^ b'))
3319, 32com2an 484 . . . 4 ((b' ^ a) v (b' ^ a')) C (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
34 comanr1 464 . . . . . . . 8 b' C (b' ^ a)
3534comcom6 459 . . . . . . 7 b C (b' ^ a)
36 comanr1 464 . . . . . . . 8 b' C (b' ^ a')
3736comcom6 459 . . . . . . 7 b C (b' ^ a')
3835, 37com2or 483 . . . . . 6 b C ((b' ^ a) v (b' ^ a'))
3938comcom 453 . . . . 5 ((b' ^ a) v (b' ^ a')) C b
40 comor1 461 . . . . . . . 8 (b' v a) C b'
41 comor2 462 . . . . . . . 8 (b' v a) C a
4240, 41com2an 484 . . . . . . 7 (b' v a) C (b' ^ a)
4341comcom2 183 . . . . . . . 8 (b' v a) C a'
4440, 43com2an 484 . . . . . . 7 (b' v a) C (b' ^ a')
4542, 44com2or 483 . . . . . 6 (b' v a) C ((b' ^ a) v (b' ^ a'))
4645comcom 453 . . . . 5 ((b' ^ a) v (b' ^ a')) C (b' v a)
4739, 46com2an 484 . . . 4 ((b' ^ a) v (b' ^ a')) C (b ^ (b' v a))
4833, 47fh2 470 . . 3 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a))))
49 coman2 186 . . . . . . . . . 10 (b' ^ a) C a
50 coman1 185 . . . . . . . . . 10 (b' ^ a) C b'
5149, 50com2or 483 . . . . . . . . 9 (b' ^ a) C (a v b')
5250comcom7 460 . . . . . . . . . 10 (b' ^ a) C b
5349, 52com2or 483 . . . . . . . . 9 (b' ^ a) C (a v b)
5451, 53com2an 484 . . . . . . . 8 (b' ^ a) C ((a v b') ^ (a v b))
5549comcom2 183 . . . . . . . . 9 (b' ^ a) C a'
5649, 50com2an 484 . . . . . . . . 9 (b' ^ a) C (a ^ b')
5755, 56com2or 483 . . . . . . . 8 (b' ^ a) C (a' v (a ^ b'))
5854, 57com2an 484 . . . . . . 7 (b' ^ a) C (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
5950, 55com2an 484 . . . . . . 7 (b' ^ a) C (b' ^ a')
6058, 59fh2 470 . . . . . 6 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) = (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a')))
61 anass 76 . . . . . . . . 9 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) = (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a)))
62 ancom 74 . . . . . . . . . . . 12 ((a' v (a ^ b')) ^ (b' ^ a)) = ((b' ^ a) ^ (a' v (a ^ b')))
63 ancom 74 . . . . . . . . . . . . . 14 (b' ^ a) = (a ^ b')
64 ax-a2 31 . . . . . . . . . . . . . 14 (a' v (a ^ b')) = ((a ^ b') v a')
6563, 642an 79 . . . . . . . . . . . . 13 ((b' ^ a) ^ (a' v (a ^ b'))) = ((a ^ b') ^ ((a ^ b') v a'))
66 anabs 121 . . . . . . . . . . . . 13 ((a ^ b') ^ ((a ^ b') v a')) = (a ^ b')
6765, 66ax-r2 36 . . . . . . . . . . . 12 ((b' ^ a) ^ (a' v (a ^ b'))) = (a ^ b')
6862, 67ax-r2 36 . . . . . . . . . . 11 ((a' v (a ^ b')) ^ (b' ^ a)) = (a ^ b')
6968lan 77 . . . . . . . . . 10 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a))) = (((a v b') ^ (a v b)) ^ (a ^ b'))
70 ancom 74 . . . . . . . . . . 11 (((a v b') ^ (a v b)) ^ (a ^ b')) = ((a ^ b') ^ ((a v b') ^ (a v b)))
71 lea 160 . . . . . . . . . . . . 13 (a ^ b') =< a
72 leo 158 . . . . . . . . . . . . . 14 a =< (a v b')
73 leo 158 . . . . . . . . . . . . . 14 a =< (a v b)
7472, 73ler2an 173 . . . . . . . . . . . . 13 a =< ((a v b') ^ (a v b))
7571, 74letr 137 . . . . . . . . . . . 12 (a ^ b') =< ((a v b') ^ (a v b))
7675df2le2 136 . . . . . . . . . . 11 ((a ^ b') ^ ((a v b') ^ (a v b))) = (a ^ b')
7770, 76ax-r2 36 . . . . . . . . . 10 (((a v b') ^ (a v b)) ^ (a ^ b')) = (a ^ b')
7869, 77ax-r2 36 . . . . . . . . 9 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b' ^ a))) = (a ^ b')
7961, 78ax-r2 36 . . . . . . . 8 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) = (a ^ b')
80 an32 83 . . . . . . . . 9 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a')) = ((((a v b') ^ (a v b)) ^ (b' ^ a')) ^ (a' v (a ^ b')))
81 anass 76 . . . . . . . . . . . 12 (((a v b') ^ (a v b)) ^ (b' ^ a')) = ((a v b') ^ ((a v b) ^ (b' ^ a')))
82 ax-a2 31 . . . . . . . . . . . . . . . 16 (a v b) = (b v a)
83 oran 87 . . . . . . . . . . . . . . . . . 18 (b v a) = (b' ^ a')'
8483ax-r1 35 . . . . . . . . . . . . . . . . 17 (b' ^ a')' = (b v a)
8584con3 68 . . . . . . . . . . . . . . . 16 (b' ^ a') = (b v a)'
8682, 852an 79 . . . . . . . . . . . . . . 15 ((a v b) ^ (b' ^ a')) = ((b v a) ^ (b v a)')
87 dff 101 . . . . . . . . . . . . . . . 16 0 = ((b v a) ^ (b v a)')
8887ax-r1 35 . . . . . . . . . . . . . . 15 ((b v a) ^ (b v a)') = 0
8986, 88ax-r2 36 . . . . . . . . . . . . . 14 ((a v b) ^ (b' ^ a')) = 0
9089lan 77 . . . . . . . . . . . . 13 ((a v b') ^ ((a v b) ^ (b' ^ a'))) = ((a v b') ^ 0)
91 an0 108 . . . . . . . . . . . . 13 ((a v b') ^ 0) = 0
9290, 91ax-r2 36 . . . . . . . . . . . 12 ((a v b') ^ ((a v b) ^ (b' ^ a'))) = 0
9381, 92ax-r2 36 . . . . . . . . . . 11 (((a v b') ^ (a v b)) ^ (b' ^ a')) = 0
9493ran 78 . . . . . . . . . 10 ((((a v b') ^ (a v b)) ^ (b' ^ a')) ^ (a' v (a ^ b'))) = (0 ^ (a' v (a ^ b')))
95 an0r 109 . . . . . . . . . 10 (0 ^ (a' v (a ^ b'))) = 0
9694, 95ax-r2 36 . . . . . . . . 9 ((((a v b') ^ (a v b)) ^ (b' ^ a')) ^ (a' v (a ^ b'))) = 0
9780, 96ax-r2 36 . . . . . . . 8 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a')) = 0
9879, 972or 72 . . . . . . 7 (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a'))) = ((a ^ b') v 0)
99 or0 102 . . . . . . 7 ((a ^ b') v 0) = (a ^ b')
10098, 99ax-r2 36 . . . . . 6 (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a)) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b' ^ a'))) = (a ^ b')
10160, 100ax-r2 36 . . . . 5 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) = (a ^ b')
102 anass 76 . . . . . 6 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a))) = (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b ^ (b' v a))))
103 anass 76 . . . . . . . . . 10 (((a' v (a ^ b')) ^ b) ^ (b' v a)) = ((a' v (a ^ b')) ^ (b ^ (b' v a)))
104103ax-r1 35 . . . . . . . . 9 ((a' v (a ^ b')) ^ (b ^ (b' v a))) = (((a' v (a ^ b')) ^ b) ^ (b' v a))
10564ran 78 . . . . . . . . . . . 12 ((a' v (a ^ b')) ^ b) = (((a ^ b') v a') ^ b)
10625comcom7 460 . . . . . . . . . . . . . 14 (a ^ b') C b
107106, 28fh2r 474 . . . . . . . . . . . . 13 (((a ^ b') v a') ^ b) = (((a ^ b') ^ b) v (a' ^ b))
108 anass 76 . . . . . . . . . . . . . . . 16 ((a ^ b') ^ b) = (a ^ (b' ^ b))
109 ancom 74 . . . . . . . . . . . . . . . . . . 19 (b' ^ b) = (b ^ b')
110 dff 101 . . . . . . . . . . . . . . . . . . . 20 0 = (b ^ b')
111110ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (b ^ b') = 0
112109, 111ax-r2 36 . . . . . . . . . . . . . . . . . 18 (b' ^ b) = 0
113112lan 77 . . . . . . . . . . . . . . . . 17 (a ^ (b' ^ b)) = (a ^ 0)
114 an0 108 . . . . . . . . . . . . . . . . 17 (a ^ 0) = 0
115113, 114ax-r2 36 . . . . . . . . . . . . . . . 16 (a ^ (b' ^ b)) = 0
116108, 115ax-r2 36 . . . . . . . . . . . . . . 15 ((a ^ b') ^ b) = 0
117 ancom 74 . . . . . . . . . . . . . . 15 (a' ^ b) = (b ^ a')
118116, 1172or 72 . . . . . . . . . . . . . 14 (((a ^ b') ^ b) v (a' ^ b)) = (0 v (b ^ a'))
119 or0r 103 . . . . . . . . . . . . . 14 (0 v (b ^ a')) = (b ^ a')
120118, 119ax-r2 36 . . . . . . . . . . . . 13 (((a ^ b') ^ b) v (a' ^ b)) = (b ^ a')
121107, 120ax-r2 36 . . . . . . . . . . . 12 (((a ^ b') v a') ^ b) = (b ^ a')
122105, 121ax-r2 36 . . . . . . . . . . 11 ((a' v (a ^ b')) ^ b) = (b ^ a')
123122ran 78 . . . . . . . . . 10 (((a' v (a ^ b')) ^ b) ^ (b' v a)) = ((b ^ a') ^ (b' v a))
124 anor1 88 . . . . . . . . . . . . . 14 (b ^ a') = (b' v a)'
125124ax-r1 35 . . . . . . . . . . . . 13 (b' v a)' = (b ^ a')
126125con3 68 . . . . . . . . . . . 12 (b' v a) = (b ^ a')'
127126lan 77 . . . . . . . . . . 11 ((b ^ a') ^ (b' v a)) = ((b ^ a') ^ (b ^ a')')
128 dff 101 . . . . . . . . . . . 12 0 = ((b ^ a') ^ (b ^ a')')
129128ax-r1 35 . . . . . . . . . . 11 ((b ^ a') ^ (b ^ a')') = 0
130127, 129ax-r2 36 . . . . . . . . . 10 ((b ^ a') ^ (b' v a)) = 0
131123, 130ax-r2 36 . . . . . . . . 9 (((a' v (a ^ b')) ^ b) ^ (b' v a)) = 0
132104, 131ax-r2 36 . . . . . . . 8 ((a' v (a ^ b')) ^ (b ^ (b' v a))) = 0
133132lan 77 . . . . . . 7 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b ^ (b' v a)))) = (((a v b') ^ (a v b)) ^ 0)
134 an0 108 . . . . . . 7 (((a v b') ^ (a v b)) ^ 0) = 0
135133, 134ax-r2 36 . . . . . 6 (((a v b') ^ (a v b)) ^ ((a' v (a ^ b')) ^ (b ^ (b' v a)))) = 0
136102, 135ax-r2 36 . . . . 5 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a))) = 0
137101, 1362or 72 . . . 4 (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a)))) = ((a ^ b') v 0)
138137, 99ax-r2 36 . . 3 (((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ ((b' ^ a) v (b' ^ a'))) v ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (b ^ (b' v a)))) = (a ^ b')
13948, 138ax-r2 36 . 2 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b' ^ a) v (b' ^ a')) v (b ^ (b' v a)))) = (a ^ b')
1403, 139ax-r2 36 1 ((a ->3 b)' ^ (b ->3 a)) = (a ^ b')
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  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:  ud3lem1  570
  Copyright terms: Public domain W3C validator