Step | Hyp | Ref
| Expression |
1 | | cycpmconjs.c |
. . 3
β’ πΆ = (π β (β‘β― β {π})) |
2 | | cycpmconjs.s |
. . 3
β’ π = (SymGrpβπ·) |
3 | | cycpmconjs.n |
. . 3
β’ π = (β―βπ·) |
4 | | cycpmconjs.m |
. . 3
β’ π = (toCycβπ·) |
5 | | cycpmconjs.b |
. . 3
β’ π΅ = (Baseβπ) |
6 | | cycpmconjs.a |
. . 3
β’ + =
(+gβπ) |
7 | | cycpmconjs.l |
. . 3
β’ β =
(-gβπ) |
8 | | cycpmconjs.p |
. . 3
β’ (π β π β (0...π)) |
9 | | cycpmconjs.d |
. . 3
β’ (π β π· β Fin) |
10 | | cycpmconjs.q |
. . 3
β’ (π β π β πΆ) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cycpmconjslem2 32053 |
. 2
β’ (π β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
12 | | cycpmconjs.t |
. . . . . 6
β’ (π β π β πΆ) |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 12 | cycpmconjslem2 32053 |
. . . . 5
β’ (π β βπ‘(π‘:(0..^π)β1-1-ontoβπ· β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
14 | 13 | ad2antrr 725 |
. . . 4
β’ (((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β βπ‘(π‘:(0..^π)β1-1-ontoβπ· β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
15 | 9 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β π· β Fin) |
16 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β π:(0..^π)β1-1-ontoβπ·) |
17 | | f1ocnv 6797 |
. . . . . . . . 9
β’ (π‘:(0..^π)β1-1-ontoβπ· β β‘π‘:π·β1-1-ontoβ(0..^π)) |
18 | 17 | ad2antlr 726 |
. . . . . . . 8
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β β‘π‘:π·β1-1-ontoβ(0..^π)) |
19 | | f1oco 6808 |
. . . . . . . 8
β’ ((π:(0..^π)β1-1-ontoβπ· β§ β‘π‘:π·β1-1-ontoβ(0..^π)) β (π β β‘π‘):π·β1-1-ontoβπ·) |
20 | 16, 18, 19 | syl2anc 585 |
. . . . . . 7
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β β‘π‘):π·β1-1-ontoβπ·) |
21 | 2, 5 | elsymgbas 19160 |
. . . . . . . 8
β’ (π· β Fin β ((π β β‘π‘) β π΅ β (π β β‘π‘):π·β1-1-ontoβπ·)) |
22 | 21 | biimpar 479 |
. . . . . . 7
β’ ((π· β Fin β§ (π β β‘π‘):π·β1-1-ontoβπ·) β (π β β‘π‘) β π΅) |
23 | 15, 20, 22 | syl2anc 585 |
. . . . . 6
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β β‘π‘) β π΅) |
24 | | simpr 486 |
. . . . . . . . 9
β’
((((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π = (π β β‘π‘)) β π = (π β β‘π‘)) |
25 | 24 | oveq1d 7373 |
. . . . . . . 8
β’
((((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π = (π β β‘π‘)) β (π + π) = ((π β β‘π‘) + π)) |
26 | 25, 24 | oveq12d 7376 |
. . . . . . 7
β’
((((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π = (π β β‘π‘)) β ((π + π) β π) = (((π β β‘π‘) + π) β (π β β‘π‘))) |
27 | 26 | eqeq2d 2744 |
. . . . . 6
β’
((((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π = (π β β‘π‘)) β (π = ((π + π) β π) β π = (((π β β‘π‘) + π) β (π β β‘π‘)))) |
28 | | simpllr 775 |
. . . . . . . . . 10
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) |
29 | | simpr 486 |
. . . . . . . . . 10
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) |
30 | 28, 29 | eqtr4d 2776 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((β‘π β π) β π) = ((β‘π‘ β π) β π‘)) |
31 | 30 | coeq1d 5818 |
. . . . . . . 8
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((β‘π β π) β π) β β‘π) = (((β‘π‘ β π) β π‘) β β‘π)) |
32 | 31 | coeq2d 5819 |
. . . . . . 7
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β (((β‘π β π) β π) β β‘π)) = (π β (((β‘π‘ β π) β π‘) β β‘π))) |
33 | | coass 6218 |
. . . . . . . . 9
β’ ((π β (β‘π β π)) β (π β β‘π)) = (π β ((β‘π β π) β (π β β‘π))) |
34 | | coass 6218 |
. . . . . . . . . 10
β’ ((π β β‘π) β π) = (π β (β‘π β π)) |
35 | 34 | coeq1i 5816 |
. . . . . . . . 9
β’ (((π β β‘π) β π) β (π β β‘π)) = ((π β (β‘π β π)) β (π β β‘π)) |
36 | | coass 6218 |
. . . . . . . . . 10
β’ (((β‘π β π) β π) β β‘π) = ((β‘π β π) β (π β β‘π)) |
37 | 36 | coeq2i 5817 |
. . . . . . . . 9
β’ (π β (((β‘π β π) β π) β β‘π)) = (π β ((β‘π β π) β (π β β‘π))) |
38 | 33, 35, 37 | 3eqtr4ri 2772 |
. . . . . . . 8
β’ (π β (((β‘π β π) β π) β β‘π)) = (((π β β‘π) β π) β (π β β‘π)) |
39 | | f1ococnv2 6812 |
. . . . . . . . . . . . 13
β’ (π:(0..^π)β1-1-ontoβπ· β (π β β‘π) = ( I βΎ π·)) |
40 | 16, 39 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β β‘π) = ( I βΎ π·)) |
41 | 40 | coeq1d 5818 |
. . . . . . . . . . 11
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π β β‘π) β π) = (( I βΎ π·) β π)) |
42 | 1, 2, 3, 4, 5 | cycpmgcl 32051 |
. . . . . . . . . . . . . . . 16
β’ ((π· β Fin β§ π β (0...π)) β πΆ β π΅) |
43 | 9, 8, 42 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β πΆ β π΅) |
44 | 43, 10 | sseldd 3946 |
. . . . . . . . . . . . . 14
β’ (π β π β π΅) |
45 | 2, 5 | elsymgbas 19160 |
. . . . . . . . . . . . . . 15
β’ (π· β Fin β (π β π΅ β π:π·β1-1-ontoβπ·)) |
46 | 45 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ ((π· β Fin β§ π β π΅) β π:π·β1-1-ontoβπ·) |
47 | 9, 44, 46 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β π:π·β1-1-ontoβπ·) |
48 | | f1of 6785 |
. . . . . . . . . . . . 13
β’ (π:π·β1-1-ontoβπ· β π:π·βΆπ·) |
49 | | fcoi2 6718 |
. . . . . . . . . . . . 13
β’ (π:π·βΆπ· β (( I βΎ π·) β π) = π) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β (( I βΎ π·) β π) = π) |
51 | 50 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (( I βΎ π·) β π) = π) |
52 | 41, 51 | eqtrd 2773 |
. . . . . . . . . 10
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π β β‘π) β π) = π) |
53 | 52, 40 | coeq12d 5821 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π) β π) β (π β β‘π)) = (π β ( I βΎ π·))) |
54 | | fcoi1 6717 |
. . . . . . . . . . 11
β’ (π:π·βΆπ· β (π β ( I βΎ π·)) = π) |
55 | 47, 48, 54 | 3syl 18 |
. . . . . . . . . 10
β’ (π β (π β ( I βΎ π·)) = π) |
56 | 55 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β ( I βΎ π·)) = π) |
57 | 53, 56 | eqtrd 2773 |
. . . . . . . 8
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π) β π) β (π β β‘π)) = π) |
58 | 38, 57 | eqtrid 2785 |
. . . . . . 7
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β (((β‘π β π) β π) β β‘π)) = π) |
59 | | coass 6218 |
. . . . . . . . 9
β’ ((π β (β‘π‘ β π)) β (π‘ β β‘π)) = (π β ((β‘π‘ β π) β (π‘ β β‘π))) |
60 | | coass 6218 |
. . . . . . . . . 10
β’ ((π β β‘π‘) β π) = (π β (β‘π‘ β π)) |
61 | 60 | coeq1i 5816 |
. . . . . . . . 9
β’ (((π β β‘π‘) β π) β (π‘ β β‘π)) = ((π β (β‘π‘ β π)) β (π‘ β β‘π)) |
62 | | coass 6218 |
. . . . . . . . . 10
β’ (((β‘π‘ β π) β π‘) β β‘π) = ((β‘π‘ β π) β (π‘ β β‘π)) |
63 | 62 | coeq2i 5817 |
. . . . . . . . 9
β’ (π β (((β‘π‘ β π) β π‘) β β‘π)) = (π β ((β‘π‘ β π) β (π‘ β β‘π))) |
64 | 59, 61, 63 | 3eqtr4i 2771 |
. . . . . . . 8
β’ (((π β β‘π‘) β π) β (π‘ β β‘π)) = (π β (((β‘π‘ β π) β π‘) β β‘π)) |
65 | 43, 12 | sseldd 3946 |
. . . . . . . . . . . 12
β’ (π β π β π΅) |
66 | 65 | ad4antr 731 |
. . . . . . . . . . 11
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β π β π΅) |
67 | 2, 5, 6 | symgov 19170 |
. . . . . . . . . . 11
β’ (((π β β‘π‘) β π΅ β§ π β π΅) β ((π β β‘π‘) + π) = ((π β β‘π‘) β π)) |
68 | 23, 66, 67 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π β β‘π‘) + π) = ((π β β‘π‘) β π)) |
69 | 68 | oveq1d 7373 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π‘) + π) β (π β β‘π‘)) = (((π β β‘π‘) β π) β (π β β‘π‘))) |
70 | 2 | symggrp 19187 |
. . . . . . . . . . . . . 14
β’ (π· β Fin β π β Grp) |
71 | 9, 70 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β Grp) |
72 | 71 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β π β Grp) |
73 | 5, 6 | grpcl 18761 |
. . . . . . . . . . . 12
β’ ((π β Grp β§ (π β β‘π‘) β π΅ β§ π β π΅) β ((π β β‘π‘) + π) β π΅) |
74 | 72, 23, 66, 73 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π β β‘π‘) + π) β π΅) |
75 | 68, 74 | eqeltrrd 2835 |
. . . . . . . . . 10
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π β β‘π‘) β π) β π΅) |
76 | 2, 5, 7 | symgsubg 31987 |
. . . . . . . . . 10
β’ ((((π β β‘π‘) β π) β π΅ β§ (π β β‘π‘) β π΅) β (((π β β‘π‘) β π) β (π β β‘π‘)) = (((π β β‘π‘) β π) β β‘(π β β‘π‘))) |
77 | 75, 23, 76 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π‘) β π) β (π β β‘π‘)) = (((π β β‘π‘) β π) β β‘(π β β‘π‘))) |
78 | | cnvco 5842 |
. . . . . . . . . . . 12
β’ β‘(π β β‘π‘) = (β‘β‘π‘ β β‘π) |
79 | | f1orel 6788 |
. . . . . . . . . . . . . 14
β’ (π‘:(0..^π)β1-1-ontoβπ· β Rel π‘) |
80 | | dfrel2 6142 |
. . . . . . . . . . . . . 14
β’ (Rel
π‘ β β‘β‘π‘ = π‘) |
81 | 79, 80 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π‘:(0..^π)β1-1-ontoβπ· β β‘β‘π‘ = π‘) |
82 | 81 | coeq1d 5818 |
. . . . . . . . . . . 12
β’ (π‘:(0..^π)β1-1-ontoβπ· β (β‘β‘π‘ β β‘π) = (π‘ β β‘π)) |
83 | 78, 82 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π‘:(0..^π)β1-1-ontoβπ· β β‘(π β β‘π‘) = (π‘ β β‘π)) |
84 | 83 | coeq2d 5819 |
. . . . . . . . . 10
β’ (π‘:(0..^π)β1-1-ontoβπ· β (((π β β‘π‘) β π) β β‘(π β β‘π‘)) = (((π β β‘π‘) β π) β (π‘ β β‘π))) |
85 | 84 | ad2antlr 726 |
. . . . . . . . 9
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π‘) β π) β β‘(π β β‘π‘)) = (((π β β‘π‘) β π) β (π‘ β β‘π))) |
86 | 69, 77, 85 | 3eqtrrd 2778 |
. . . . . . . 8
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (((π β β‘π‘) β π) β (π‘ β β‘π)) = (((π β β‘π‘) + π) β (π β β‘π‘))) |
87 | 64, 86 | eqtr3id 2787 |
. . . . . . 7
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β (π β (((β‘π‘ β π) β π‘) β β‘π)) = (((π β β‘π‘) + π) β (π β β‘π‘))) |
88 | 32, 58, 87 | 3eqtr3d 2781 |
. . . . . 6
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β π = (((π β β‘π‘) + π) β (π β β‘π‘))) |
89 | 23, 27, 88 | rspcedvd 3582 |
. . . . 5
β’
(((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ π‘:(0..^π)β1-1-ontoβπ·) β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β βπ β π΅ π = ((π + π) β π)) |
90 | 89 | anasss 468 |
. . . 4
β’ ((((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β§ (π‘:(0..^π)β1-1-ontoβπ· β§ ((β‘π‘ β π) β π‘) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) β βπ β π΅ π = ((π + π) β π)) |
91 | 14, 90 | exlimddv 1939 |
. . 3
β’ (((π β§ π:(0..^π)β1-1-ontoβπ·) β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β βπ β π΅ π = ((π + π) β π)) |
92 | 91 | anasss 468 |
. 2
β’ ((π β§ (π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) β βπ β π΅ π = ((π + π) β π)) |
93 | 11, 92 | exlimddv 1939 |
1
β’ (π β βπ β π΅ π = ((π + π) β π)) |