Step | Hyp | Ref
| Expression |
1 | | fzofi 13886 |
. . . . 5
β’
(0..^π) β
Fin |
2 | | diffi 9130 |
. . . . 5
β’
((0..^π) β Fin
β ((0..^π) β dom
π’) β
Fin) |
3 | 1, 2 | mp1i 13 |
. . . 4
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β ((0..^π) β dom π’) β Fin) |
4 | | cycpmconjs.d |
. . . . . 6
β’ (π β π· β Fin) |
5 | | diffi 9130 |
. . . . . 6
β’ (π· β Fin β (π· β ran π’) β Fin) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π β (π· β ran π’) β Fin) |
7 | 6 | ad2antrr 725 |
. . . 4
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (π· β ran π’) β Fin) |
8 | | cycpmconjs.n |
. . . . . . . . . 10
β’ π = (β―βπ·) |
9 | | hashcl 14263 |
. . . . . . . . . . 11
β’ (π· β Fin β
(β―βπ·) β
β0) |
10 | 4, 9 | syl 17 |
. . . . . . . . . 10
β’ (π β (β―βπ·) β
β0) |
11 | 8, 10 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β π β
β0) |
12 | | hashfzo0 14337 |
. . . . . . . . 9
β’ (π β β0
β (β―β(0..^π)) = π) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β (β―β(0..^π)) = π) |
14 | 13, 8 | eqtrdi 2793 |
. . . . . . 7
β’ (π β (β―β(0..^π)) = (β―βπ·)) |
15 | 14 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―β(0..^π)) = (β―βπ·)) |
16 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) |
17 | 16 | elin1d 4163 |
. . . . . . . . 9
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
18 | | elrabi 3644 |
. . . . . . . . 9
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β π’ β Word π·) |
19 | | wrdfin 14427 |
. . . . . . . . 9
β’ (π’ β Word π· β π’ β Fin) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ β Fin) |
21 | | id 22 |
. . . . . . . . . . . . 13
β’ (π€ = π’ β π€ = π’) |
22 | | dmeq 5864 |
. . . . . . . . . . . . 13
β’ (π€ = π’ β dom π€ = dom π’) |
23 | | eqidd 2738 |
. . . . . . . . . . . . 13
β’ (π€ = π’ β π· = π·) |
24 | 21, 22, 23 | f1eq123d 6781 |
. . . . . . . . . . . 12
β’ (π€ = π’ β (π€:dom π€β1-1βπ· β π’:dom π’β1-1βπ·)) |
25 | 24 | elrab 3650 |
. . . . . . . . . . 11
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β (π’ β Word π· β§ π’:dom π’β1-1βπ·)) |
26 | 25 | simprbi 498 |
. . . . . . . . . 10
β’ (π’ β {π€ β Word π· β£ π€:dom π€β1-1βπ·} β π’:dom π’β1-1βπ·) |
27 | 17, 26 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’:dom π’β1-1βπ·) |
28 | | f1fun 6745 |
. . . . . . . . 9
β’ (π’:dom π’β1-1βπ· β Fun π’) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β Fun π’) |
30 | | hashfun 14344 |
. . . . . . . . 9
β’ (π’ β Fin β (Fun π’ β (β―βπ’) = (β―βdom π’))) |
31 | 30 | biimpa 478 |
. . . . . . . 8
β’ ((π’ β Fin β§ Fun π’) β (β―βπ’) = (β―βdom π’)) |
32 | 20, 29, 31 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) = (β―βdom π’)) |
33 | 16 | dmexd 7847 |
. . . . . . . 8
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β dom π’ β V) |
34 | | hashf1rn 14259 |
. . . . . . . 8
β’ ((dom
π’ β V β§ π’:dom π’β1-1βπ·) β (β―βπ’) = (β―βran π’)) |
35 | 33, 27, 34 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) = (β―βran π’)) |
36 | 32, 35 | eqtr3d 2779 |
. . . . . 6
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βdom π’) = (β―βran π’)) |
37 | 15, 36 | oveq12d 7380 |
. . . . 5
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β ((β―β(0..^π)) β (β―βdom
π’)) = ((β―βπ·) β (β―βran
π’))) |
38 | 1 | a1i 11 |
. . . . . 6
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (0..^π) β Fin) |
39 | | wrddm 14416 |
. . . . . . . 8
β’ (π’ β Word π· β dom π’ = (0..^(β―βπ’))) |
40 | 17, 18, 39 | 3syl 18 |
. . . . . . 7
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β dom π’ = (0..^(β―βπ’))) |
41 | | hashcl 14263 |
. . . . . . . . . . 11
β’ (π’ β Fin β
(β―βπ’) β
β0) |
42 | 17, 18, 19, 41 | 4syl 19 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) β
β0) |
43 | 42 | nn0zd 12532 |
. . . . . . . . 9
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) β β€) |
44 | 10 | nn0zd 12532 |
. . . . . . . . . . 11
β’ (π β (β―βπ·) β
β€) |
45 | 8, 44 | eqeltrid 2842 |
. . . . . . . . . 10
β’ (π β π β β€) |
46 | 45 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π β β€) |
47 | 4 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π· β Fin) |
48 | | wrdf 14414 |
. . . . . . . . . . . . 13
β’ (π’ β Word π· β π’:(0..^(β―βπ’))βΆπ·) |
49 | 48 | frnd 6681 |
. . . . . . . . . . . 12
β’ (π’ β Word π· β ran π’ β π·) |
50 | 17, 18, 49 | 3syl 18 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β ran π’ β π·) |
51 | | hashss 14316 |
. . . . . . . . . . 11
β’ ((π· β Fin β§ ran π’ β π·) β (β―βran π’) β€ (β―βπ·)) |
52 | 47, 50, 51 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βran π’) β€ (β―βπ·)) |
53 | 8 | a1i 11 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π = (β―βπ·)) |
54 | 52, 35, 53 | 3brtr4d 5142 |
. . . . . . . . 9
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) β€ π) |
55 | | eluz1 12774 |
. . . . . . . . . 10
β’
((β―βπ’)
β β€ β (π
β (β€β₯β(β―βπ’)) β (π β β€ β§ (β―βπ’) β€ π))) |
56 | 55 | biimpar 479 |
. . . . . . . . 9
β’
(((β―βπ’)
β β€ β§ (π
β β€ β§ (β―βπ’) β€ π)) β π β
(β€β₯β(β―βπ’))) |
57 | 43, 46, 54, 56 | syl12anc 836 |
. . . . . . . 8
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π β
(β€β₯β(β―βπ’))) |
58 | | fzoss2 13607 |
. . . . . . . 8
β’ (π β
(β€β₯β(β―βπ’)) β (0..^(β―βπ’)) β (0..^π)) |
59 | 57, 58 | syl 17 |
. . . . . . 7
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (0..^(β―βπ’)) β (0..^π)) |
60 | 40, 59 | eqsstrd 3987 |
. . . . . 6
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β dom π’ β (0..^π)) |
61 | | hashssdif 14319 |
. . . . . 6
β’
(((0..^π) β Fin
β§ dom π’ β
(0..^π)) β
(β―β((0..^π)
β dom π’)) =
((β―β(0..^π))
β (β―βdom π’))) |
62 | 38, 60, 61 | syl2anc 585 |
. . . . 5
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―β((0..^π) β dom π’)) = ((β―β(0..^π)) β (β―βdom π’))) |
63 | | hashssdif 14319 |
. . . . . 6
β’ ((π· β Fin β§ ran π’ β π·) β (β―β(π· β ran π’)) = ((β―βπ·) β (β―βran π’))) |
64 | 47, 50, 63 | syl2anc 585 |
. . . . 5
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―β(π· β ran π’)) = ((β―βπ·) β (β―βran π’))) |
65 | 37, 62, 64 | 3eqtr4d 2787 |
. . . 4
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―β((0..^π) β dom π’)) = (β―β(π· β ran π’))) |
66 | | hasheqf1o 14256 |
. . . . 5
β’
((((0..^π) β
dom π’) β Fin β§
(π· β ran π’) β Fin) β
((β―β((0..^π)
β dom π’)) =
(β―β(π· β
ran π’)) β βπ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’))) |
67 | 66 | biimpa 478 |
. . . 4
β’
(((((0..^π) β
dom π’) β Fin β§
(π· β ran π’) β Fin) β§
(β―β((0..^π)
β dom π’)) =
(β―β(π· β
ran π’))) β
βπ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) |
68 | 3, 7, 65, 67 | syl21anc 837 |
. . 3
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β βπ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) |
69 | 27 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π’:dom π’β1-1βπ·) |
70 | | f1f1orn 6800 |
. . . . . . 7
β’ (π’:dom π’β1-1βπ· β π’:dom π’β1-1-ontoβran
π’) |
71 | 69, 70 | syl 17 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π’:dom π’β1-1-ontoβran
π’) |
72 | | simpr 486 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) |
73 | | disjdif 4436 |
. . . . . . 7
β’ (dom
π’ β© ((0..^π) β dom π’)) = β
|
74 | 73 | a1i 11 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (dom π’ β© ((0..^π) β dom π’)) = β
) |
75 | | disjdif 4436 |
. . . . . . 7
β’ (ran
π’ β© (π· β ran π’)) = β
|
76 | 75 | a1i 11 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (ran π’ β© (π· β ran π’)) = β
) |
77 | | f1oun 6808 |
. . . . . 6
β’ (((π’:dom π’β1-1-ontoβran
π’ β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β§ ((dom π’ β© ((0..^π) β dom π’)) = β
β§ (ran π’ β© (π· β ran π’)) = β
)) β (π’ βͺ π):(dom π’ βͺ ((0..^π) β dom π’))β1-1-ontoβ(ran
π’ βͺ (π· β ran π’))) |
78 | 71, 72, 74, 76, 77 | syl22anc 838 |
. . . . 5
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π’ βͺ π):(dom π’ βͺ ((0..^π) β dom π’))β1-1-ontoβ(ran
π’ βͺ (π· β ran π’))) |
79 | | eqidd 2738 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π’ βͺ π) = (π’ βͺ π)) |
80 | 60 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β dom π’ β (0..^π)) |
81 | | undif 4446 |
. . . . . . 7
β’ (dom
π’ β (0..^π) β (dom π’ βͺ ((0..^π) β dom π’)) = (0..^π)) |
82 | 80, 81 | sylib 217 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (dom π’ βͺ ((0..^π) β dom π’)) = (0..^π)) |
83 | | undif 4446 |
. . . . . . . 8
β’ (ran
π’ β π· β (ran π’ βͺ (π· β ran π’)) = π·) |
84 | 50, 83 | sylib 217 |
. . . . . . 7
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (ran π’ βͺ (π· β ran π’)) = π·) |
85 | 84 | adantr 482 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (ran π’ βͺ (π· β ran π’)) = π·) |
86 | 79, 82, 85 | f1oeq123d 6783 |
. . . . 5
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ βͺ π):(dom π’ βͺ ((0..^π) β dom π’))β1-1-ontoβ(ran
π’ βͺ (π· β ran π’)) β (π’ βͺ π):(0..^π)β1-1-ontoβπ·)) |
87 | 78, 86 | mpbid 231 |
. . . 4
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π’ βͺ π):(0..^π)β1-1-ontoβπ·) |
88 | | f1ocnv 6801 |
. . . . . . . . . 10
β’ ((π’ βͺ π):(0..^π)β1-1-ontoβπ· β β‘(π’ βͺ π):π·β1-1-ontoβ(0..^π)) |
89 | 87, 88 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘(π’ βͺ π):π·β1-1-ontoβ(0..^π)) |
90 | | cycpmconjs.p |
. . . . . . . . . . . . 13
β’ (π β π β (0...π)) |
91 | | cycpmconjs.c |
. . . . . . . . . . . . . 14
β’ πΆ = (π β (β‘β― β {π})) |
92 | | cycpmconjs.s |
. . . . . . . . . . . . . 14
β’ π = (SymGrpβπ·) |
93 | | cycpmconjs.m |
. . . . . . . . . . . . . 14
β’ π = (toCycβπ·) |
94 | | cycpmconjs.b |
. . . . . . . . . . . . . 14
β’ π΅ = (Baseβπ) |
95 | 91, 92, 8, 93, 94 | cycpmgcl 32044 |
. . . . . . . . . . . . 13
β’ ((π· β Fin β§ π β (0...π)) β πΆ β π΅) |
96 | 4, 90, 95 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β πΆ β π΅) |
97 | | cycpmconjs.q |
. . . . . . . . . . . 12
β’ (π β π β πΆ) |
98 | 96, 97 | sseldd 3950 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
99 | 92, 94 | symgbasf1o 19163 |
. . . . . . . . . . 11
β’ (π β π΅ β π:π·β1-1-ontoβπ·) |
100 | 98, 99 | syl 17 |
. . . . . . . . . 10
β’ (π β π:π·β1-1-ontoβπ·) |
101 | 100 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π:π·β1-1-ontoβπ·) |
102 | | f1oco 6812 |
. . . . . . . . 9
β’ ((β‘(π’ βͺ π):π·β1-1-ontoβ(0..^π) β§ π:π·β1-1-ontoβπ·) β (β‘(π’ βͺ π) β π):π·β1-1-ontoβ(0..^π)) |
103 | 89, 101, 102 | syl2anc 585 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘(π’ βͺ π) β π):π·β1-1-ontoβ(0..^π)) |
104 | | f1oco 6812 |
. . . . . . . 8
β’ (((β‘(π’ βͺ π) β π):π·β1-1-ontoβ(0..^π) β§ (π’ βͺ π):(0..^π)β1-1-ontoβπ·) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)):(0..^π)β1-1-ontoβ(0..^π)) |
105 | 103, 87, 104 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)):(0..^π)β1-1-ontoβ(0..^π)) |
106 | | f1ofun 6791 |
. . . . . . 7
β’ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)):(0..^π)β1-1-ontoβ(0..^π) β Fun ((β‘(π’ βͺ π) β π) β (π’ βͺ π))) |
107 | | funrel 6523 |
. . . . . . 7
β’ (Fun
((β‘(π’ βͺ π) β π) β (π’ βͺ π)) β Rel ((β‘(π’ βͺ π) β π) β (π’ βͺ π))) |
108 | 105, 106,
107 | 3syl 18 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β Rel ((β‘(π’ βͺ π) β π) β (π’ βͺ π))) |
109 | | f1odm 6793 |
. . . . . . . 8
β’ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)):(0..^π)β1-1-ontoβ(0..^π) β dom ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = (0..^π)) |
110 | 105, 109 | syl 17 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β dom ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = (0..^π)) |
111 | | fzosplit 13612 |
. . . . . . . . 9
β’ (π β (0...π) β (0..^π) = ((0..^π) βͺ (π..^π))) |
112 | 90, 111 | syl 17 |
. . . . . . . 8
β’ (π β (0..^π) = ((0..^π) βͺ (π..^π))) |
113 | 112 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (0..^π) = ((0..^π) βͺ (π..^π))) |
114 | 110, 113 | eqtrd 2777 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β dom ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((0..^π) βͺ (π..^π))) |
115 | | fzodisj 13613 |
. . . . . . 7
β’
((0..^π) β©
(π..^π)) = β
|
116 | | reldisjun 31563 |
. . . . . . 7
β’ ((Rel
((β‘(π’ βͺ π) β π) β (π’ βͺ π)) β§ dom ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((0..^π) βͺ (π..^π)) β§ ((0..^π) β© (π..^π)) = β
) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) βͺ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)))) |
117 | 115, 116 | mp3an3 1451 |
. . . . . 6
β’ ((Rel
((β‘(π’ βͺ π) β π) β (π’ βͺ π)) β§ dom ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((0..^π) βͺ (π..^π))) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) βͺ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)))) |
118 | 108, 114,
117 | syl2anc 585 |
. . . . 5
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) βͺ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)))) |
119 | | resco 6207 |
. . . . . . . 8
β’ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) = ((β‘(π’ βͺ π) β π) β ((π’ βͺ π) βΎ (0..^π))) |
120 | 119 | a1i 11 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) = ((β‘(π’ βͺ π) β π) β ((π’ βͺ π) βΎ (0..^π)))) |
121 | 17, 18 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ β Word π·) |
122 | | wrdfn 14423 |
. . . . . . . . . . . 12
β’ (π’ β Word π· β π’ Fn (0..^(β―βπ’))) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ Fn (0..^(β―βπ’))) |
124 | 16 | elin2d 4164 |
. . . . . . . . . . . . . 14
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ β (β‘β― β {π})) |
125 | | hashf 14245 |
. . . . . . . . . . . . . . . 16
β’
β―:VβΆ(β0 βͺ {+β}) |
126 | | ffn 6673 |
. . . . . . . . . . . . . . . 16
β’
(β―:VβΆ(β0 βͺ {+β}) β β―
Fn V) |
127 | | fniniseg 7015 |
. . . . . . . . . . . . . . . 16
β’ (β―
Fn V β (π’ β
(β‘β― β {π}) β (π’ β V β§ (β―βπ’) = π))) |
128 | 125, 126,
127 | mp2b 10 |
. . . . . . . . . . . . . . 15
β’ (π’ β (β‘β― β {π}) β (π’ β V β§ (β―βπ’) = π)) |
129 | 128 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π’ β (β‘β― β {π}) β (β―βπ’) = π) |
130 | 124, 129 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (β―βπ’) = π) |
131 | 130 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (0..^(β―βπ’)) = (0..^π)) |
132 | 131 | fneq2d 6601 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (π’ Fn (0..^(β―βπ’)) β π’ Fn (0..^π))) |
133 | 123, 132 | mpbid 231 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β π’ Fn (0..^π)) |
134 | 133 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π’ Fn (0..^π)) |
135 | | f1ofn 6790 |
. . . . . . . . . 10
β’ (π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’) β π Fn ((0..^π) β dom π’)) |
136 | 72, 135 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π Fn ((0..^π) β dom π’)) |
137 | 40, 131 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β dom π’ = (0..^π)) |
138 | 137 | ineq1d 4176 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (dom π’ β© ((0..^π) β dom π’)) = ((0..^π) β© ((0..^π) β dom π’))) |
139 | 73 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β (dom π’ β© ((0..^π) β dom π’)) = β
) |
140 | 138, 139 | eqtr3d 2779 |
. . . . . . . . . 10
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β ((0..^π) β© ((0..^π) β dom π’)) = β
) |
141 | 140 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((0..^π) β© ((0..^π) β dom π’)) = β
) |
142 | | fnunres1 31566 |
. . . . . . . . 9
β’ ((π’ Fn (0..^π) β§ π Fn ((0..^π) β dom π’) β§ ((0..^π) β© ((0..^π) β dom π’)) = β
) β ((π’ βͺ π) βΎ (0..^π)) = π’) |
143 | 134, 136,
141, 142 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ βͺ π) βΎ (0..^π)) = π’) |
144 | 143 | coeq2d 5823 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β ((π’ βͺ π) βΎ (0..^π))) = ((β‘(π’ βͺ π) β π) β π’)) |
145 | | resco 6207 |
. . . . . . . . . . 11
β’ ((β‘(π’ βͺ π) β π) βΎ ran π’) = (β‘(π’ βͺ π) β (π βΎ ran π’)) |
146 | | resco 6207 |
. . . . . . . . . . . . 13
β’ ((β‘π’ β (πβπ’)) βΎ ran π’) = (β‘π’ β ((πβπ’) βΎ ran π’)) |
147 | 146 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π’ β (πβπ’)) βΎ ran π’) = (β‘π’ β ((πβπ’) βΎ ran π’))) |
148 | | cnvun 6100 |
. . . . . . . . . . . . . . 15
β’ β‘(π’ βͺ π) = (β‘π’ βͺ β‘π) |
149 | 148 | reseq1i 5938 |
. . . . . . . . . . . . . 14
β’ (β‘(π’ βͺ π) βΎ ran π’) = ((β‘π’ βͺ β‘π) βΎ ran π’) |
150 | | f1ocnv 6801 |
. . . . . . . . . . . . . . . 16
β’ (π’:dom π’β1-1-ontoβran
π’ β β‘π’:ran π’β1-1-ontoβdom
π’) |
151 | | f1ofn 6790 |
. . . . . . . . . . . . . . . 16
β’ (β‘π’:ran π’β1-1-ontoβdom
π’ β β‘π’ Fn ran π’) |
152 | 71, 150, 151 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘π’ Fn ran π’) |
153 | | f1ocnv 6801 |
. . . . . . . . . . . . . . . 16
β’ (π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’) β β‘π:(π· β ran π’)β1-1-ontoβ((0..^π) β dom π’)) |
154 | | f1ofn 6790 |
. . . . . . . . . . . . . . . 16
β’ (β‘π:(π· β ran π’)β1-1-ontoβ((0..^π) β dom π’) β β‘π Fn (π· β ran π’)) |
155 | 72, 153, 154 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘π Fn (π· β ran π’)) |
156 | | fnunres1 31566 |
. . . . . . . . . . . . . . 15
β’ ((β‘π’ Fn ran π’ β§ β‘π Fn (π· β ran π’) β§ (ran π’ β© (π· β ran π’)) = β
) β ((β‘π’ βͺ β‘π) βΎ ran π’) = β‘π’) |
157 | 152, 155,
76, 156 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π’ βͺ β‘π) βΎ ran π’) = β‘π’) |
158 | 149, 157 | eqtr2id 2790 |
. . . . . . . . . . . . 13
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘π’ = (β‘(π’ βͺ π) βΎ ran π’)) |
159 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (πβπ’) = π) |
160 | 159 | reseq1d 5941 |
. . . . . . . . . . . . 13
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((πβπ’) βΎ ran π’) = (π βΎ ran π’)) |
161 | 158, 160 | coeq12d 5825 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘π’ β ((πβπ’) βΎ ran π’)) = ((β‘(π’ βͺ π) βΎ ran π’) β (π βΎ ran π’))) |
162 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π· β Fin) |
163 | 121 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β π’ β Word π·) |
164 | 93, 162, 163, 69 | tocycfvres1 32001 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((πβπ’) βΎ ran π’) = ((π’ cyclShift 1) β β‘π’)) |
165 | 160, 164 | eqtr3d 2779 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π βΎ ran π’) = ((π’ cyclShift 1) β β‘π’)) |
166 | 165 | rneqd 5898 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran (π βΎ ran π’) = ran ((π’ cyclShift 1) β β‘π’)) |
167 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β 1 β β€) |
168 | | cshf1o 31858 |
. . . . . . . . . . . . . . . . . 18
β’ ((π’ β Word π· β§ π’:dom π’β1-1βπ· β§ 1 β β€) β (π’ cyclShift 1):dom π’β1-1-ontoβran
π’) |
169 | 163, 69, 167, 168 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π’ cyclShift 1):dom π’β1-1-ontoβran
π’) |
170 | 71, 150 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘π’:ran π’β1-1-ontoβdom
π’) |
171 | | f1oco 6812 |
. . . . . . . . . . . . . . . . 17
β’ (((π’ cyclShift 1):dom π’β1-1-ontoβran
π’ β§ β‘π’:ran π’β1-1-ontoβdom
π’) β ((π’ cyclShift 1) β β‘π’):ran π’β1-1-ontoβran
π’) |
172 | 169, 170,
171 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ cyclShift 1) β β‘π’):ran π’β1-1-ontoβran
π’) |
173 | | f1ofo 6796 |
. . . . . . . . . . . . . . . 16
β’ (((π’ cyclShift 1) β β‘π’):ran π’β1-1-ontoβran
π’ β ((π’ cyclShift 1) β β‘π’):ran π’βontoβran π’) |
174 | | forn 6764 |
. . . . . . . . . . . . . . . 16
β’ (((π’ cyclShift 1) β β‘π’):ran π’βontoβran π’ β ran ((π’ cyclShift 1) β β‘π’) = ran π’) |
175 | 172, 173,
174 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran ((π’ cyclShift 1) β β‘π’) = ran π’) |
176 | 166, 175 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran (π βΎ ran π’) = ran π’) |
177 | | ssid 3971 |
. . . . . . . . . . . . . 14
β’ ran π’ β ran π’ |
178 | 176, 177 | eqsstrdi 4003 |
. . . . . . . . . . . . 13
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran (π βΎ ran π’) β ran π’) |
179 | | cores 6206 |
. . . . . . . . . . . . 13
β’ (ran
(π βΎ ran π’) β ran π’ β ((β‘(π’ βͺ π) βΎ ran π’) β (π βΎ ran π’)) = (β‘(π’ βͺ π) β (π βΎ ran π’))) |
180 | 178, 179 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) βΎ ran π’) β (π βΎ ran π’)) = (β‘(π’ βͺ π) β (π βΎ ran π’))) |
181 | 147, 161,
180 | 3eqtrrd 2782 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘(π’ βͺ π) β (π βΎ ran π’)) = ((β‘π’ β (πβπ’)) βΎ ran π’)) |
182 | 145, 181 | eqtrid 2789 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) βΎ ran π’) = ((β‘π’ β (πβπ’)) βΎ ran π’)) |
183 | 182 | coeq1d 5822 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) βΎ ran π’) β π’) = (((β‘π’ β (πβπ’)) βΎ ran π’) β π’)) |
184 | | cores 6206 |
. . . . . . . . . 10
β’ (ran
π’ β ran π’ β (((β‘π’ β (πβπ’)) βΎ ran π’) β π’) = ((β‘π’ β (πβπ’)) β π’)) |
185 | 177, 184 | mp1i 13 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘π’ β (πβπ’)) βΎ ran π’) β π’) = ((β‘π’ β (πβπ’)) β π’)) |
186 | 183, 185 | eqtrd 2777 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) βΎ ran π’) β π’) = ((β‘π’ β (πβπ’)) β π’)) |
187 | | cores 6206 |
. . . . . . . . 9
β’ (ran
π’ β ran π’ β (((β‘(π’ βͺ π) β π) βΎ ran π’) β π’) = ((β‘(π’ βͺ π) β π) β π’)) |
188 | 177, 187 | mp1i 13 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) βΎ ran π’) β π’) = ((β‘(π’ βͺ π) β π) β π’)) |
189 | 130 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β―βπ’) = π) |
190 | 91, 92, 8, 93, 162, 163, 69, 189 | cycpmconjslem1 32045 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π’ β (πβπ’)) β π’) = (( I βΎ (0..^π)) cyclShift 1)) |
191 | 186, 188,
190 | 3eqtr3d 2785 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β π’) = (( I βΎ (0..^π)) cyclShift 1)) |
192 | 120, 144,
191 | 3eqtrd 2781 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) = (( I βΎ (0..^π)) cyclShift 1)) |
193 | | resco 6207 |
. . . . . . . 8
β’ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)) = ((β‘(π’ βͺ π) β π) β ((π’ βͺ π) βΎ (π..^π))) |
194 | 137 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β dom π’ = (0..^π)) |
195 | 194 | difeq2d 4087 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((0..^π) β dom π’) = ((0..^π) β (0..^π))) |
196 | | fzodif1 31738 |
. . . . . . . . . . . . . 14
β’ (π β (0...π) β ((0..^π) β (0..^π)) = (π..^π)) |
197 | 90, 196 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((0..^π) β (0..^π)) = (π..^π)) |
198 | 197 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((0..^π) β (0..^π)) = (π..^π)) |
199 | 195, 198 | eqtrd 2777 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((0..^π) β dom π’) = (π..^π)) |
200 | 199 | reseq2d 5942 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ βͺ π) βΎ ((0..^π) β dom π’)) = ((π’ βͺ π) βΎ (π..^π))) |
201 | | fnunres2 31636 |
. . . . . . . . . . 11
β’ ((π’ Fn (0..^π) β§ π Fn ((0..^π) β dom π’) β§ ((0..^π) β© ((0..^π) β dom π’)) = β
) β ((π’ βͺ π) βΎ ((0..^π) β dom π’)) = π) |
202 | 134, 136,
141, 201 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ βͺ π) βΎ ((0..^π) β dom π’)) = π) |
203 | 200, 202 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((π’ βͺ π) βΎ (π..^π)) = π) |
204 | 203 | coeq2d 5823 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β ((π’ βͺ π) βΎ (π..^π))) = ((β‘(π’ βͺ π) β π) β π)) |
205 | 193, 204 | eqtrid 2789 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)) = ((β‘(π’ βͺ π) β π) β π)) |
206 | 148 | reseq1i 5938 |
. . . . . . . . . . . 12
β’ (β‘(π’ βͺ π) βΎ (π· β ran π’)) = ((β‘π’ βͺ β‘π) βΎ (π· β ran π’)) |
207 | | fnunres2 31636 |
. . . . . . . . . . . . 13
β’ ((β‘π’ Fn ran π’ β§ β‘π Fn (π· β ran π’) β§ (ran π’ β© (π· β ran π’)) = β
) β ((β‘π’ βͺ β‘π) βΎ (π· β ran π’)) = β‘π) |
208 | 152, 155,
76, 207 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π’ βͺ β‘π) βΎ (π· β ran π’)) = β‘π) |
209 | 206, 208 | eqtrid 2789 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘(π’ βͺ π) βΎ (π· β ran π’)) = β‘π) |
210 | 159 | reseq1d 5941 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((πβπ’) βΎ (π· β ran π’)) = (π βΎ (π· β ran π’))) |
211 | 93, 162, 163, 69 | tocycfvres2 32002 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((πβπ’) βΎ (π· β ran π’)) = ( I βΎ (π· β ran π’))) |
212 | 210, 211 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (π βΎ (π· β ran π’)) = ( I βΎ (π· β ran π’))) |
213 | 209, 212 | coeq12d 5825 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) βΎ (π· β ran π’)) β (π βΎ (π· β ran π’))) = (β‘π β ( I βΎ (π· β ran π’)))) |
214 | 212 | rneqd 5898 |
. . . . . . . . . . . . 13
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran (π βΎ (π· β ran π’)) = ran ( I βΎ (π· β ran π’))) |
215 | | rnresi 6032 |
. . . . . . . . . . . . . 14
β’ ran ( I
βΎ (π· β ran
π’)) = (π· β ran π’) |
216 | 215 | eqimssi 4007 |
. . . . . . . . . . . . 13
β’ ran ( I
βΎ (π· β ran
π’)) β (π· β ran π’) |
217 | 214, 216 | eqsstrdi 4003 |
. . . . . . . . . . . 12
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran (π βΎ (π· β ran π’)) β (π· β ran π’)) |
218 | | cores 6206 |
. . . . . . . . . . . 12
β’ (ran
(π βΎ (π· β ran π’)) β (π· β ran π’) β ((β‘(π’ βͺ π) βΎ (π· β ran π’)) β (π βΎ (π· β ran π’))) = (β‘(π’ βͺ π) β (π βΎ (π· β ran π’)))) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) βΎ (π· β ran π’)) β (π βΎ (π· β ran π’))) = (β‘(π’ βͺ π) β (π βΎ (π· β ran π’)))) |
220 | | resco 6207 |
. . . . . . . . . . 11
β’ ((β‘(π’ βͺ π) β π) βΎ (π· β ran π’)) = (β‘(π’ βͺ π) β (π βΎ (π· β ran π’))) |
221 | 219, 220 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) βΎ (π· β ran π’)) β (π βΎ (π· β ran π’))) = ((β‘(π’ βͺ π) β π) βΎ (π· β ran π’))) |
222 | 213, 221 | eqtr3d 2779 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘π β ( I βΎ (π· β ran π’))) = ((β‘(π’ βͺ π) β π) βΎ (π· β ran π’))) |
223 | 222 | coeq1d 5822 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π β ( I βΎ (π· β ran π’))) β π) = (((β‘(π’ βͺ π) β π) βΎ (π· β ran π’)) β π)) |
224 | | f1of 6789 |
. . . . . . . . . . . 12
β’ (β‘π:(π· β ran π’)β1-1-ontoβ((0..^π) β dom π’) β β‘π:(π· β ran π’)βΆ((0..^π) β dom π’)) |
225 | 72, 153, 224 | 3syl 18 |
. . . . . . . . . . 11
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β β‘π:(π· β ran π’)βΆ((0..^π) β dom π’)) |
226 | | fcoi1 6721 |
. . . . . . . . . . 11
β’ (β‘π:(π· β ran π’)βΆ((0..^π) β dom π’) β (β‘π β ( I βΎ (π· β ran π’))) = β‘π) |
227 | 225, 226 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘π β ( I βΎ (π· β ran π’))) = β‘π) |
228 | 227 | coeq1d 5822 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π β ( I βΎ (π· β ran π’))) β π) = (β‘π β π)) |
229 | | f1ococnv1 6818 |
. . . . . . . . . 10
β’ (π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’) β (β‘π β π) = ( I βΎ ((0..^π) β dom π’))) |
230 | 72, 229 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (β‘π β π) = ( I βΎ ((0..^π) β dom π’))) |
231 | 199 | reseq2d 5942 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ( I βΎ ((0..^π) β dom π’)) = ( I βΎ (π..^π))) |
232 | 228, 230,
231 | 3eqtrd 2781 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘π β ( I βΎ (π· β ran π’))) β π) = ( I βΎ (π..^π))) |
233 | | f1of 6789 |
. . . . . . . . . 10
β’ (π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’) β π:((0..^π) β dom π’)βΆ(π· β ran π’)) |
234 | | frn 6680 |
. . . . . . . . . 10
β’ (π:((0..^π) β dom π’)βΆ(π· β ran π’) β ran π β (π· β ran π’)) |
235 | 72, 233, 234 | 3syl 18 |
. . . . . . . . 9
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ran π β (π· β ran π’)) |
236 | | cores 6206 |
. . . . . . . . 9
β’ (ran
π β (π· β ran π’) β (((β‘(π’ βͺ π) β π) βΎ (π· β ran π’)) β π) = ((β‘(π’ βͺ π) β π) β π)) |
237 | 235, 236 | syl 17 |
. . . . . . . 8
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) βΎ (π· β ran π’)) β π) = ((β‘(π’ βͺ π) β π) β π)) |
238 | 223, 232,
237 | 3eqtr3rd 2786 |
. . . . . . 7
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β π) = ( I βΎ (π..^π))) |
239 | 205, 238 | eqtrd 2777 |
. . . . . 6
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π)) = ( I βΎ (π..^π))) |
240 | 192, 239 | uneq12d 4129 |
. . . . 5
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (0..^π)) βͺ (((β‘(π’ βͺ π) β π) β (π’ βͺ π)) βΎ (π..^π))) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) |
241 | 118, 240 | eqtrd 2777 |
. . . 4
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) |
242 | | vex 3452 |
. . . . . 6
β’ π’ β V |
243 | | vex 3452 |
. . . . . 6
β’ π β V |
244 | 242, 243 | unex 7685 |
. . . . 5
β’ (π’ βͺ π) β V |
245 | | f1oeq1 6777 |
. . . . . 6
β’ (π = (π’ βͺ π) β (π:(0..^π)β1-1-ontoβπ· β (π’ βͺ π):(0..^π)β1-1-ontoβπ·)) |
246 | | cnveq 5834 |
. . . . . . . . 9
β’ (π = (π’ βͺ π) β β‘π = β‘(π’ βͺ π)) |
247 | 246 | coeq1d 5822 |
. . . . . . . 8
β’ (π = (π’ βͺ π) β (β‘π β π) = (β‘(π’ βͺ π) β π)) |
248 | | id 22 |
. . . . . . . 8
β’ (π = (π’ βͺ π) β π = (π’ βͺ π)) |
249 | 247, 248 | coeq12d 5825 |
. . . . . . 7
β’ (π = (π’ βͺ π) β ((β‘π β π) β π) = ((β‘(π’ βͺ π) β π) β (π’ βͺ π))) |
250 | 249 | eqeq1d 2739 |
. . . . . 6
β’ (π = (π’ βͺ π) β (((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))) β ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
251 | 245, 250 | anbi12d 632 |
. . . . 5
β’ (π = (π’ βͺ π) β ((π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β ((π’ βͺ π):(0..^π)β1-1-ontoβπ· β§ ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))))) |
252 | 244, 251 | spcev 3568 |
. . . 4
β’ (((π’ βͺ π):(0..^π)β1-1-ontoβπ· β§ ((β‘(π’ βͺ π) β π) β (π’ βͺ π)) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π)))) β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
253 | 87, 241, 252 | syl2anc 585 |
. . 3
β’ ((((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β§ π:((0..^π) β dom π’)β1-1-ontoβ(π· β ran π’)) β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
254 | 68, 253 | exlimddv 1939 |
. 2
β’ (((π β§ π’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))) β§ (πβπ’) = π) β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |
255 | | nfcv 2908 |
. . 3
β’
β²π’π |
256 | 93, 92, 94 | tocycf 32008 |
. . . 4
β’ (π· β Fin β π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅) |
257 | | ffn 6673 |
. . . 4
β’ (π:{π€ β Word π· β£ π€:dom π€β1-1βπ·}βΆπ΅ β π Fn {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
258 | 4, 256, 257 | 3syl 18 |
. . 3
β’ (π β π Fn {π€ β Word π· β£ π€:dom π€β1-1βπ·}) |
259 | 97, 91 | eleqtrdi 2848 |
. . 3
β’ (π β π β (π β (β‘β― β {π}))) |
260 | 255, 258,
259 | fvelimad 6914 |
. 2
β’ (π β βπ’ β ({π€ β Word π· β£ π€:dom π€β1-1βπ·} β© (β‘β― β {π}))(πβπ’) = π) |
261 | 254, 260 | r19.29a 3160 |
1
β’ (π β βπ(π:(0..^π)β1-1-ontoβπ· β§ ((β‘π β π) β π) = ((( I βΎ (0..^π)) cyclShift 1) βͺ ( I βΎ (π..^π))))) |