[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ud5lem1a 586
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud5lem1a ((a ->5 b) ^ (b ->5 a)) = ((a ^ b) v (a' ^ b'))
Proof of Theorem ud5lem1a
StepHypRef Expression
1 df-i5 48 . . 3 (a ->5 b) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
2 df-i5 48 . . 3 (b ->5 a) = (((b ^ a) v (b' ^ a)) v (b' ^ a'))
31, 22an 79 . 2 ((a ->5 b) ^ (b ->5 a)) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (((b ^ a) v (b' ^ a)) v (b' ^ a')))
4 ax-a2 31 . . . 4 (((b ^ a) v (b' ^ a)) v (b' ^ a')) = ((b' ^ a') v ((b ^ a) v (b' ^ a)))
54lan 77 . . 3 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (((b ^ a) v (b' ^ a)) v (b' ^ a'))) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b' ^ a') v ((b ^ a) v (b' ^ a))))
6 coman2 186 . . . . . . . . . 10 (a ^ b) C b
76comcom2 183 . . . . . . . . 9 (a ^ b) C b'
8 coman1 185 . . . . . . . . . 10 (a ^ b) C a
98comcom2 183 . . . . . . . . 9 (a ^ b) C a'
107, 9com2an 484 . . . . . . . 8 (a ^ b) C (b' ^ a')
1110comcom 453 . . . . . . 7 (b' ^ a') C (a ^ b)
12 coman2 186 . . . . . . . . . 10 (a' ^ b) C b
1312comcom2 183 . . . . . . . . 9 (a' ^ b) C b'
14 coman1 185 . . . . . . . . 9 (a' ^ b) C a'
1513, 14com2an 484 . . . . . . . 8 (a' ^ b) C (b' ^ a')
1615comcom 453 . . . . . . 7 (b' ^ a') C (a' ^ b)
1711, 16com2or 483 . . . . . 6 (b' ^ a') C ((a ^ b) v (a' ^ b))
18 coman2 186 . . . . . . 7 (b' ^ a') C a'
19 coman1 185 . . . . . . 7 (b' ^ a') C b'
2018, 19com2an 484 . . . . . 6 (b' ^ a') C (a' ^ b')
2117, 20com2or 483 . . . . 5 (b' ^ a') C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
22 coman1 185 . . . . . . . . 9 (b ^ a) C b
2322comcom2 183 . . . . . . . 8 (b ^ a) C b'
24 coman2 186 . . . . . . . . 9 (b ^ a) C a
2524comcom2 183 . . . . . . . 8 (b ^ a) C a'
2623, 25com2an 484 . . . . . . 7 (b ^ a) C (b' ^ a')
2726comcom 453 . . . . . 6 (b' ^ a') C (b ^ a)
28 coman1 185 . . . . . . . 8 (b' ^ a) C b'
29 coman2 186 . . . . . . . . 9 (b' ^ a) C a
3029comcom2 183 . . . . . . . 8 (b' ^ a) C a'
3128, 30com2an 484 . . . . . . 7 (b' ^ a) C (b' ^ a')
3231comcom 453 . . . . . 6 (b' ^ a') C (b' ^ a)
3327, 32com2or 483 . . . . 5 (b' ^ a') C ((b ^ a) v (b' ^ a))
3421, 33fh2 470 . . . 4 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b' ^ a') v ((b ^ a) v (b' ^ a)))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) v ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ ((b ^ a) v (b' ^ a))))
3518comcom3 454 . . . . . . . . . . 11 (b' ^ a')' C a'
3635comcom5 458 . . . . . . . . . 10 (b' ^ a') C a
3719comcom3 454 . . . . . . . . . . 11 (b' ^ a')' C b'
3837comcom5 458 . . . . . . . . . 10 (b' ^ a') C b
3936, 38com2an 484 . . . . . . . . 9 (b' ^ a') C (a ^ b)
4018, 38com2an 484 . . . . . . . . 9 (b' ^ a') C (a' ^ b)
4139, 40com2or 483 . . . . . . . 8 (b' ^ a') C ((a ^ b) v (a' ^ b))
4241, 20fh1r 473 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) = ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a')))
4311, 16fh1r 473 . . . . . . . . . 10 (((a ^ b) v (a' ^ b)) ^ (b' ^ a')) = (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a')))
44 anass 76 . . . . . . . . . . . . 13 ((a ^ b) ^ (b' ^ a')) = (a ^ (b ^ (b' ^ a')))
45 anass 76 . . . . . . . . . . . . . . . 16 ((b ^ b') ^ a') = (b ^ (b' ^ a'))
4645ax-r1 35 . . . . . . . . . . . . . . 15 (b ^ (b' ^ a')) = ((b ^ b') ^ a')
4746lan 77 . . . . . . . . . . . . . 14 (a ^ (b ^ (b' ^ a'))) = (a ^ ((b ^ b') ^ a'))
48 ancom 74 . . . . . . . . . . . . . . . . 17 ((b ^ b') ^ a') = (a' ^ (b ^ b'))
49 dff 101 . . . . . . . . . . . . . . . . . . . 20 0 = (b ^ b')
5049ax-r1 35 . . . . . . . . . . . . . . . . . . 19 (b ^ b') = 0
5150lan 77 . . . . . . . . . . . . . . . . . 18 (a' ^ (b ^ b')) = (a' ^ 0)
52 an0 108 . . . . . . . . . . . . . . . . . 18 (a' ^ 0) = 0
5351, 52ax-r2 36 . . . . . . . . . . . . . . . . 17 (a' ^ (b ^ b')) = 0
5448, 53ax-r2 36 . . . . . . . . . . . . . . . 16 ((b ^ b') ^ a') = 0
5554lan 77 . . . . . . . . . . . . . . 15 (a ^ ((b ^ b') ^ a')) = (a ^ 0)
56 an0 108 . . . . . . . . . . . . . . 15 (a ^ 0) = 0
5755, 56ax-r2 36 . . . . . . . . . . . . . 14 (a ^ ((b ^ b') ^ a')) = 0
5847, 57ax-r2 36 . . . . . . . . . . . . 13 (a ^ (b ^ (b' ^ a'))) = 0
5944, 58ax-r2 36 . . . . . . . . . . . 12 ((a ^ b) ^ (b' ^ a')) = 0
60 anass 76 . . . . . . . . . . . . 13 ((a' ^ b) ^ (b' ^ a')) = (a' ^ (b ^ (b' ^ a')))
6146lan 77 . . . . . . . . . . . . . 14 (a' ^ (b ^ (b' ^ a'))) = (a' ^ ((b ^ b') ^ a'))
6254lan 77 . . . . . . . . . . . . . . 15 (a' ^ ((b ^ b') ^ a')) = (a' ^ 0)
6362, 52ax-r2 36 . . . . . . . . . . . . . 14 (a' ^ ((b ^ b') ^ a')) = 0
6461, 63ax-r2 36 . . . . . . . . . . . . 13 (a' ^ (b ^ (b' ^ a'))) = 0
6560, 64ax-r2 36 . . . . . . . . . . . 12 ((a' ^ b) ^ (b' ^ a')) = 0
6659, 652or 72 . . . . . . . . . . 11 (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a'))) = (0 v 0)
67 or0 102 . . . . . . . . . . 11 (0 v 0) = 0
6866, 67ax-r2 36 . . . . . . . . . 10 (((a ^ b) ^ (b' ^ a')) v ((a' ^ b) ^ (b' ^ a'))) = 0
6943, 68ax-r2 36 . . . . . . . . 9 (((a ^ b) v (a' ^ b)) ^ (b' ^ a')) = 0
70 ancom 74 . . . . . . . . . . 11 (b' ^ a') = (a' ^ b')
7170lan 77 . . . . . . . . . 10 ((a' ^ b') ^ (b' ^ a')) = ((a' ^ b') ^ (a' ^ b'))
72 anidm 111 . . . . . . . . . 10 ((a' ^ b') ^ (a' ^ b')) = (a' ^ b')
7371, 72ax-r2 36 . . . . . . . . 9 ((a' ^ b') ^ (b' ^ a')) = (a' ^ b')
7469, 732or 72 . . . . . . . 8 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a'))) = (0 v (a' ^ b'))
75 ax-a2 31 . . . . . . . . 9 (0 v (a' ^ b')) = ((a' ^ b') v 0)
76 or0 102 . . . . . . . . 9 ((a' ^ b') v 0) = (a' ^ b')
7775, 76ax-r2 36 . . . . . . . 8 (0 v (a' ^ b')) = (a' ^ b')
7874, 77ax-r2 36 . . . . . . 7 ((((a ^ b) v (a' ^ b)) ^ (b' ^ a')) v ((a' ^ b') ^ (b' ^ a'))) = (a' ^ b')
7942, 78ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) ^ (b' ^ a')) = (a' ^ b')
8024, 22com2an 484 . . . . . . . . . 10 (b ^ a) C (a ^ b)
8125, 22com2an 484 . . . . . . . . . 10 (b ^ a) C (a' ^ b)
8280, 81com2or 483 . . . . . . . . 9 (b ^ a) C ((a ^ b) v (a' ^ b))
8325, 23com2an 484 . . . . . . . . 9 (b ^ a) C (a' ^ b')
8482, 83com2or 483 . . . . . . . 8 (b ^ a) C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
8523, 24com2an 484 . . . . . . . 8 (b ^ a) C (b' ^ a)
8684, 85fh2 470 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^