# Metamath Proof Explorer

## Theorem cycpmco2f1

Description: The word U used in cycpmco2 is injective, so it can represent a cycle and form a cyclic permutation ( MU ) . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ${⊢}{M}=\mathrm{toCyc}\left({D}\right)$
cycpmco2.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
cycpmco2.d ${⊢}{\phi }\to {D}\in {V}$
cycpmco2.w ${⊢}{\phi }\to {W}\in \mathrm{dom}{M}$
cycpmco2.i ${⊢}{\phi }\to {I}\in \left({D}\setminus \mathrm{ran}{W}\right)$
cycpmco2.j ${⊢}{\phi }\to {J}\in \mathrm{ran}{W}$
cycpmco2.e ${⊢}{E}={{W}}^{-1}\left({J}\right)+1$
cycpmco2.1 ${⊢}{U}={W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩$
Assertion cycpmco2f1 ${⊢}{\phi }\to {U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}$

### Proof

Step Hyp Ref Expression
1 cycpmco2.c ${⊢}{M}=\mathrm{toCyc}\left({D}\right)$
2 cycpmco2.s ${⊢}{S}=\mathrm{SymGrp}\left({D}\right)$
3 cycpmco2.d ${⊢}{\phi }\to {D}\in {V}$
4 cycpmco2.w ${⊢}{\phi }\to {W}\in \mathrm{dom}{M}$
5 cycpmco2.i ${⊢}{\phi }\to {I}\in \left({D}\setminus \mathrm{ran}{W}\right)$
6 cycpmco2.j ${⊢}{\phi }\to {J}\in \mathrm{ran}{W}$
7 cycpmco2.e ${⊢}{E}={{W}}^{-1}\left({J}\right)+1$
8 cycpmco2.1 ${⊢}{U}={W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩$
9 ssrab2 ${⊢}\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}\subseteq \mathrm{Word}{D}$
10 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
11 1 2 10 tocycf ${⊢}{D}\in {V}\to {M}:\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}⟶{\mathrm{Base}}_{{S}}$
12 3 11 syl ${⊢}{\phi }\to {M}:\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}⟶{\mathrm{Base}}_{{S}}$
13 12 fdmd ${⊢}{\phi }\to \mathrm{dom}{M}=\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}$
14 4 13 eleqtrd ${⊢}{\phi }\to {W}\in \left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}$
15 9 14 sseldi ${⊢}{\phi }\to {W}\in \mathrm{Word}{D}$
16 pfxcl ${⊢}{W}\in \mathrm{Word}{D}\to {W}\mathrm{prefix}{E}\in \mathrm{Word}{D}$
17 15 16 syl ${⊢}{\phi }\to {W}\mathrm{prefix}{E}\in \mathrm{Word}{D}$
18 5 eldifad ${⊢}{\phi }\to {I}\in {D}$
19 18 s1cld ${⊢}{\phi }\to ⟨“{I}”⟩\in \mathrm{Word}{D}$
20 ccatcl ${⊢}\left({W}\mathrm{prefix}{E}\in \mathrm{Word}{D}\wedge ⟨“{I}”⟩\in \mathrm{Word}{D}\right)\to \left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\in \mathrm{Word}{D}$
21 17 19 20 syl2anc ${⊢}{\phi }\to \left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\in \mathrm{Word}{D}$
22 swrdcl ${⊢}{W}\in \mathrm{Word}{D}\to {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}$
23 15 22 syl ${⊢}{\phi }\to {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}$
24 id ${⊢}{w}={W}\to {w}={W}$
25 dmeq ${⊢}{w}={W}\to \mathrm{dom}{w}=\mathrm{dom}{W}$
26 eqidd ${⊢}{w}={W}\to {D}={D}$
27 24 25 26 f1eq123d ${⊢}{w}={W}\to \left({w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}↔{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\right)$
28 27 elrab ${⊢}{W}\in \left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}↔\left({W}\in \mathrm{Word}{D}\wedge {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\right)$
29 14 28 sylib ${⊢}{\phi }\to \left({W}\in \mathrm{Word}{D}\wedge {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\right)$
30 29 simprd ${⊢}{\phi }\to {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}$
31 f1cnv ${⊢}{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\to {{W}}^{-1}:\mathrm{ran}{W}\underset{1-1 onto}{⟶}\mathrm{dom}{W}$
32 f1of ${⊢}{{W}}^{-1}:\mathrm{ran}{W}\underset{1-1 onto}{⟶}\mathrm{dom}{W}\to {{W}}^{-1}:\mathrm{ran}{W}⟶\mathrm{dom}{W}$
33 30 31 32 3syl ${⊢}{\phi }\to {{W}}^{-1}:\mathrm{ran}{W}⟶\mathrm{dom}{W}$
34 33 6 ffvelrnd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \mathrm{dom}{W}$
35 wrddm ${⊢}{W}\in \mathrm{Word}{D}\to \mathrm{dom}{W}=\left(0..^\left|{W}\right|\right)$
36 15 35 syl ${⊢}{\phi }\to \mathrm{dom}{W}=\left(0..^\left|{W}\right|\right)$
37 34 36 eleqtrd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\right|\right)$
38 fzofzp1 ${⊢}{{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\right|\right)\to {{W}}^{-1}\left({J}\right)+1\in \left(0\dots \left|{W}\right|\right)$
39 37 38 syl ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)+1\in \left(0\dots \left|{W}\right|\right)$
40 7 39 eqeltrid ${⊢}{\phi }\to {E}\in \left(0\dots \left|{W}\right|\right)$
41 15 30 40 pfxf1 ${⊢}{\phi }\to \left({W}\mathrm{prefix}{E}\right):\mathrm{dom}\left({W}\mathrm{prefix}{E}\right)\underset{1-1}{⟶}{D}$
42 18 s1f1 ${⊢}{\phi }\to ⟨“{I}”⟩:\mathrm{dom}⟨“{I}”⟩\underset{1-1}{⟶}{D}$
43 s1rn ${⊢}{I}\in {D}\to \mathrm{ran}⟨“{I}”⟩=\left\{{I}\right\}$
44 18 43 syl ${⊢}{\phi }\to \mathrm{ran}⟨“{I}”⟩=\left\{{I}\right\}$
45 44 ineq2d ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}⟨“{I}”⟩=\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}$
46 pfxrn2 ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {E}\in \left(0\dots \left|{W}\right|\right)\right)\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\subseteq \mathrm{ran}{W}$
47 15 40 46 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\subseteq \mathrm{ran}{W}$
48 47 ssrind ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}\subseteq \mathrm{ran}{W}\cap \left\{{I}\right\}$
49 5 eldifbd ${⊢}{\phi }\to ¬{I}\in \mathrm{ran}{W}$
50 disjsn ${⊢}\mathrm{ran}{W}\cap \left\{{I}\right\}=\varnothing ↔¬{I}\in \mathrm{ran}{W}$
51 49 50 sylibr ${⊢}{\phi }\to \mathrm{ran}{W}\cap \left\{{I}\right\}=\varnothing$
52 48 51 sseqtrd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}\subseteq \varnothing$
53 ss0 ${⊢}\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}\subseteq \varnothing \to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}=\varnothing$
54 52 53 syl ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \left\{{I}\right\}=\varnothing$
55 45 54 eqtrd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}⟨“{I}”⟩=\varnothing$
56 3 17 19 41 42 55 ccatf1 ${⊢}{\phi }\to \left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right):\mathrm{dom}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\underset{1-1}{⟶}{D}$
57 lencl ${⊢}{W}\in \mathrm{Word}{D}\to \left|{W}\right|\in {ℕ}_{0}$
58 nn0fz0 ${⊢}\left|{W}\right|\in {ℕ}_{0}↔\left|{W}\right|\in \left(0\dots \left|{W}\right|\right)$
59 58 biimpi ${⊢}\left|{W}\right|\in {ℕ}_{0}\to \left|{W}\right|\in \left(0\dots \left|{W}\right|\right)$
60 15 57 59 3syl ${⊢}{\phi }\to \left|{W}\right|\in \left(0\dots \left|{W}\right|\right)$
61 15 40 60 30 swrdf1 ${⊢}{\phi }\to \left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right):\mathrm{dom}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\underset{1-1}{⟶}{D}$
62 ccatrn ${⊢}\left({W}\mathrm{prefix}{E}\in \mathrm{Word}{D}\wedge ⟨“{I}”⟩\in \mathrm{Word}{D}\right)\to \mathrm{ran}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)=\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cup \mathrm{ran}⟨“{I}”⟩$
63 17 19 62 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)=\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cup \mathrm{ran}⟨“{I}”⟩$
64 63 ineq1d ${⊢}{\phi }\to \mathrm{ran}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\left(\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cup \mathrm{ran}⟨“{I}”⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
65 indir ${⊢}\left(\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cup \mathrm{ran}⟨“{I}”⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\left(\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\cup \left(\mathrm{ran}⟨“{I}”⟩\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)$
66 64 65 syl6eq ${⊢}{\phi }\to \mathrm{ran}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\left(\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\cup \left(\mathrm{ran}⟨“{I}”⟩\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)$
67 fz0ssnn0 ${⊢}\left(0\dots \left|{W}\right|\right)\subseteq {ℕ}_{0}$
68 67 40 sseldi ${⊢}{\phi }\to {E}\in {ℕ}_{0}$
69 pfxval ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {E}\in {ℕ}_{0}\right)\to {W}\mathrm{prefix}{E}={W}\mathrm{substr}⟨0,{E}⟩$
70 15 68 69 syl2anc ${⊢}{\phi }\to {W}\mathrm{prefix}{E}={W}\mathrm{substr}⟨0,{E}⟩$
71 70 rneqd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)=\mathrm{ran}\left({W}\mathrm{substr}⟨0,{E}⟩\right)$
72 71 ineq1d ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\mathrm{ran}\left({W}\mathrm{substr}⟨0,{E}⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
73 0elfz ${⊢}{E}\in {ℕ}_{0}\to 0\in \left(0\dots {E}\right)$
74 68 73 syl ${⊢}{\phi }\to 0\in \left(0\dots {E}\right)$
75 elfzuz3 ${⊢}{E}\in \left(0\dots \left|{W}\right|\right)\to \left|{W}\right|\in {ℤ}_{\ge {E}}$
76 eluzfz1 ${⊢}\left|{W}\right|\in {ℤ}_{\ge {E}}\to {E}\in \left({E}\dots \left|{W}\right|\right)$
77 40 75 76 3syl ${⊢}{\phi }\to {E}\in \left({E}\dots \left|{W}\right|\right)$
78 eluzfz2 ${⊢}\left|{W}\right|\in {ℤ}_{\ge {E}}\to \left|{W}\right|\in \left({E}\dots \left|{W}\right|\right)$
79 40 75 78 3syl ${⊢}{\phi }\to \left|{W}\right|\in \left({E}\dots \left|{W}\right|\right)$
80 15 74 40 30 77 79 swrdrndisj ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨0,{E}⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\varnothing$
81 72 80 eqtrd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\varnothing$
82 incom ${⊢}\mathrm{ran}⟨“{I}”⟩\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \mathrm{ran}⟨“{I}”⟩$
83 44 ineq2d ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \mathrm{ran}⟨“{I}”⟩=\mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}$
84 swrdrn2 ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {E}\in \left(0\dots \left|{W}\right|\right)\wedge \left|{W}\right|\in \left(0\dots \left|{W}\right|\right)\right)\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\subseteq \mathrm{ran}{W}$
85 15 40 60 84 syl3anc ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\subseteq \mathrm{ran}{W}$
86 85 ssrind ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}\subseteq \mathrm{ran}{W}\cap \left\{{I}\right\}$
87 86 51 sseqtrd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}\subseteq \varnothing$
88 ss0 ${⊢}\mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}\subseteq \varnothing \to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}=\varnothing$
89 87 88 syl ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \left\{{I}\right\}=\varnothing$
90 83 89 eqtrd ${⊢}{\phi }\to \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\cap \mathrm{ran}⟨“{I}”⟩=\varnothing$
91 82 90 syl5eq ${⊢}{\phi }\to \mathrm{ran}⟨“{I}”⟩\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\varnothing$
92 81 91 uneq12d ${⊢}{\phi }\to \left(\mathrm{ran}\left({W}\mathrm{prefix}{E}\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\cup \left(\mathrm{ran}⟨“{I}”⟩\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)=\varnothing \cup \varnothing$
93 unidm ${⊢}\varnothing \cup \varnothing =\varnothing$
94 93 a1i ${⊢}{\phi }\to \varnothing \cup \varnothing =\varnothing$
95 66 92 94 3eqtrd ${⊢}{\phi }\to \mathrm{ran}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\cap \mathrm{ran}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)=\varnothing$
96 3 21 23 56 61 95 ccatf1 ${⊢}{\phi }\to \left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right):\mathrm{dom}\left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\underset{1-1}{⟶}{D}$
97 ovexd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)+1\in \mathrm{V}$
98 7 97 eqeltrid ${⊢}{\phi }\to {E}\in \mathrm{V}$
99 splval ${⊢}\left({W}\in \mathrm{dom}{M}\wedge \left({E}\in \mathrm{V}\wedge {E}\in \mathrm{V}\wedge ⟨“{I}”⟩\in \mathrm{Word}{D}\right)\right)\to {W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
100 4 98 98 19 99 syl13anc ${⊢}{\phi }\to {W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
101 8 100 syl5eq ${⊢}{\phi }\to {U}=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
102 101 dmeqd ${⊢}{\phi }\to \mathrm{dom}{U}=\mathrm{dom}\left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)$
103 eqidd ${⊢}{\phi }\to {D}={D}$
104 101 102 103 f1eq123d ${⊢}{\phi }\to \left({U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}↔\left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right):\mathrm{dom}\left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\underset{1-1}{⟶}{D}\right)$
105 96 104 mpbird ${⊢}{\phi }\to {U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}$