# Metamath Proof Explorer

## Theorem cycpmco2

Description: The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-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 cycpmco2 ${⊢}{\phi }\to {M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)={M}\left({U}\right)$

### 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 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
10 1 2 9 tocycf ${⊢}{D}\in {V}\to {M}:\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}⟶{\mathrm{Base}}_{{S}}$
11 3 10 syl ${⊢}{\phi }\to {M}:\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}⟶{\mathrm{Base}}_{{S}}$
12 11 fdmd ${⊢}{\phi }\to \mathrm{dom}{M}=\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}$
13 4 12 eleqtrd ${⊢}{\phi }\to {W}\in \left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}$
14 11 13 ffvelrnd ${⊢}{\phi }\to {M}\left({W}\right)\in {\mathrm{Base}}_{{S}}$
15 2 9 symgbasf ${⊢}{M}\left({W}\right)\in {\mathrm{Base}}_{{S}}\to {M}\left({W}\right):{D}⟶{D}$
16 14 15 syl ${⊢}{\phi }\to {M}\left({W}\right):{D}⟶{D}$
17 16 ffnd ${⊢}{\phi }\to {M}\left({W}\right)Fn{D}$
18 5 eldifad ${⊢}{\phi }\to {I}\in {D}$
19 ssrab2 ${⊢}\left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}\subseteq \mathrm{Word}{D}$
20 19 13 sseldi ${⊢}{\phi }\to {W}\in \mathrm{Word}{D}$
21 id ${⊢}{w}={W}\to {w}={W}$
22 dmeq ${⊢}{w}={W}\to \mathrm{dom}{w}=\mathrm{dom}{W}$
23 eqidd ${⊢}{w}={W}\to {D}={D}$
24 21 22 23 f1eq123d ${⊢}{w}={W}\to \left({w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}↔{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\right)$
25 24 elrab3 ${⊢}{W}\in \mathrm{Word}{D}\to \left({W}\in \left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}↔{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\right)$
26 25 biimpa ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {W}\in \left\{{w}\in \mathrm{Word}{D}|{w}:\mathrm{dom}{w}\underset{1-1}{⟶}{D}\right\}\right)\to {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}$
27 20 13 26 syl2anc ${⊢}{\phi }\to {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}$
28 f1f ${⊢}{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\to {W}:\mathrm{dom}{W}⟶{D}$
29 27 28 syl ${⊢}{\phi }\to {W}:\mathrm{dom}{W}⟶{D}$
30 29 frnd ${⊢}{\phi }\to \mathrm{ran}{W}\subseteq {D}$
31 30 6 sseldd ${⊢}{\phi }\to {J}\in {D}$
32 5 eldifbd ${⊢}{\phi }\to ¬{I}\in \mathrm{ran}{W}$
33 nelne2 ${⊢}\left({J}\in \mathrm{ran}{W}\wedge ¬{I}\in \mathrm{ran}{W}\right)\to {J}\ne {I}$
34 6 32 33 syl2anc ${⊢}{\phi }\to {J}\ne {I}$
35 34 necomd ${⊢}{\phi }\to {I}\ne {J}$
36 1 3 18 31 35 2 cycpm2cl ${⊢}{\phi }\to {M}\left(⟨“{I}{J}”⟩\right)\in {\mathrm{Base}}_{{S}}$
37 2 9 symgbasf ${⊢}{M}\left(⟨“{I}{J}”⟩\right)\in {\mathrm{Base}}_{{S}}\to {M}\left(⟨“{I}{J}”⟩\right):{D}⟶{D}$
38 36 37 syl ${⊢}{\phi }\to {M}\left(⟨“{I}{J}”⟩\right):{D}⟶{D}$
39 38 ffnd ${⊢}{\phi }\to {M}\left(⟨“{I}{J}”⟩\right)Fn{D}$
40 38 frnd ${⊢}{\phi }\to \mathrm{ran}{M}\left(⟨“{I}{J}”⟩\right)\subseteq {D}$
41 fnco ${⊢}\left({M}\left({W}\right)Fn{D}\wedge {M}\left(⟨“{I}{J}”⟩\right)Fn{D}\wedge \mathrm{ran}{M}\left(⟨“{I}{J}”⟩\right)\subseteq {D}\right)\to \left({M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)\right)Fn{D}$
42 17 39 40 41 syl3anc ${⊢}{\phi }\to \left({M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)\right)Fn{D}$
43 18 s1cld ${⊢}{\phi }\to ⟨“{I}”⟩\in \mathrm{Word}{D}$
44 splcl ${⊢}\left({W}\in \mathrm{Word}{D}\wedge ⟨“{I}”⟩\in \mathrm{Word}{D}\right)\to {W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩\in \mathrm{Word}{D}$
45 20 43 44 syl2anc ${⊢}{\phi }\to {W}\mathrm{splice}⟨{E},{E},⟨“{I}”⟩⟩\in \mathrm{Word}{D}$
46 8 45 eqeltrid ${⊢}{\phi }\to {U}\in \mathrm{Word}{D}$
47 1 2 3 4 5 6 7 8 cycpmco2f1 ${⊢}{\phi }\to {U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}$
48 1 3 46 47 2 cycpmcl ${⊢}{\phi }\to {M}\left({U}\right)\in {\mathrm{Base}}_{{S}}$
49 2 9 symgbasf ${⊢}{M}\left({U}\right)\in {\mathrm{Base}}_{{S}}\to {M}\left({U}\right):{D}⟶{D}$
50 48 49 syl ${⊢}{\phi }\to {M}\left({U}\right):{D}⟶{D}$
51 50 ffnd ${⊢}{\phi }\to {M}\left({U}\right)Fn{D}$
52 fvco3 ${⊢}\left({M}\left(⟨“{I}{J}”⟩\right):{D}⟶{D}\wedge {i}\in {D}\right)\to \left({M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)\right)\left({i}\right)={M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)$
53 38 52 sylan ${⊢}\left({\phi }\wedge {i}\in {D}\right)\to \left({M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)\right)\left({i}\right)={M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)$
54 1 3 18 31 35 2 cyc2fv2 ${⊢}{\phi }\to {M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)={I}$
55 54 fveq2d ${⊢}{\phi }\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)\right)={M}\left({W}\right)\left({I}\right)$
56 1 2 3 4 5 6 7 8 cycpmco2lem2 ${⊢}{\phi }\to {U}\left({E}\right)={I}$
57 f1cnv ${⊢}{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\to {{W}}^{-1}:\mathrm{ran}{W}\underset{1-1 onto}{⟶}\mathrm{dom}{W}$
58 f1of ${⊢}{{W}}^{-1}:\mathrm{ran}{W}\underset{1-1 onto}{⟶}\mathrm{dom}{W}\to {{W}}^{-1}:\mathrm{ran}{W}⟶\mathrm{dom}{W}$
59 27 57 58 3syl ${⊢}{\phi }\to {{W}}^{-1}:\mathrm{ran}{W}⟶\mathrm{dom}{W}$
60 59 6 ffvelrnd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \mathrm{dom}{W}$
61 wrddm ${⊢}{W}\in \mathrm{Word}{D}\to \mathrm{dom}{W}=\left(0..^\left|{W}\right|\right)$
62 20 61 syl ${⊢}{\phi }\to \mathrm{dom}{W}=\left(0..^\left|{W}\right|\right)$
63 60 62 eleqtrd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\right|\right)$
64 lencl ${⊢}{W}\in \mathrm{Word}{D}\to \left|{W}\right|\in {ℕ}_{0}$
65 20 64 syl ${⊢}{\phi }\to \left|{W}\right|\in {ℕ}_{0}$
66 65 nn0cnd ${⊢}{\phi }\to \left|{W}\right|\in ℂ$
67 1cnd ${⊢}{\phi }\to 1\in ℂ$
68 ovexd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)+1\in \mathrm{V}$
69 7 68 eqeltrid ${⊢}{\phi }\to {E}\in \mathrm{V}$
70 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)$
71 4 69 69 43 70 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)$
72 8 71 syl5eq ${⊢}{\phi }\to {U}=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)$
73 72 fveq2d ${⊢}{\phi }\to \left|{U}\right|=\left|\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right|$
74 pfxcl ${⊢}{W}\in \mathrm{Word}{D}\to {W}\mathrm{prefix}{E}\in \mathrm{Word}{D}$
75 20 74 syl ${⊢}{\phi }\to {W}\mathrm{prefix}{E}\in \mathrm{Word}{D}$
76 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}$
77 75 43 76 syl2anc ${⊢}{\phi }\to \left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\in \mathrm{Word}{D}$
78 swrdcl ${⊢}{W}\in \mathrm{Word}{D}\to {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}$
79 20 78 syl ${⊢}{\phi }\to {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}$
80 ccatlen ${⊢}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\in \mathrm{Word}{D}\wedge {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}\right)\to \left|\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right|=\left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|+\left|{W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right|$
81 77 79 80 syl2anc ${⊢}{\phi }\to \left|\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right|=\left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|+\left|{W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right|$
82 ccatws1len ${⊢}{W}\mathrm{prefix}{E}\in \mathrm{Word}{D}\to \left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|=\left|{W}\mathrm{prefix}{E}\right|+1$
83 20 74 82 3syl ${⊢}{\phi }\to \left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|=\left|{W}\mathrm{prefix}{E}\right|+1$
84 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)$
85 63 84 syl ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)+1\in \left(0\dots \left|{W}\right|\right)$
86 7 85 eqeltrid ${⊢}{\phi }\to {E}\in \left(0\dots \left|{W}\right|\right)$
87 pfxlen ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {E}\in \left(0\dots \left|{W}\right|\right)\right)\to \left|{W}\mathrm{prefix}{E}\right|={E}$
88 20 86 87 syl2anc ${⊢}{\phi }\to \left|{W}\mathrm{prefix}{E}\right|={E}$
89 88 oveq1d ${⊢}{\phi }\to \left|{W}\mathrm{prefix}{E}\right|+1={E}+1$
90 83 89 eqtrd ${⊢}{\phi }\to \left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|={E}+1$
91 nn0fz0 ${⊢}\left|{W}\right|\in {ℕ}_{0}↔\left|{W}\right|\in \left(0\dots \left|{W}\right|\right)$
92 65 91 sylib ${⊢}{\phi }\to \left|{W}\right|\in \left(0\dots \left|{W}\right|\right)$
93 swrdlen ${⊢}\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 \left|{W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right|=\left|{W}\right|-{E}$
94 20 86 92 93 syl3anc ${⊢}{\phi }\to \left|{W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right|=\left|{W}\right|-{E}$
95 90 94 oveq12d ${⊢}{\phi }\to \left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|+\left|{W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right|={E}+1+\left(\left|{W}\right|-{E}\right)$
96 73 81 95 3eqtrd ${⊢}{\phi }\to \left|{U}\right|={E}+1+\left(\left|{W}\right|-{E}\right)$
97 fz0ssnn0 ${⊢}\left(0\dots \left|{W}\right|\right)\subseteq {ℕ}_{0}$
98 97 86 sseldi ${⊢}{\phi }\to {E}\in {ℕ}_{0}$
99 98 nn0zd ${⊢}{\phi }\to {E}\in ℤ$
100 99 peano2zd ${⊢}{\phi }\to {E}+1\in ℤ$
101 100 zcnd ${⊢}{\phi }\to {E}+1\in ℂ$
102 98 nn0cnd ${⊢}{\phi }\to {E}\in ℂ$
103 101 66 102 addsubassd ${⊢}{\phi }\to \left({E}+1\right)+\left|{W}\right|-{E}={E}+1+\left(\left|{W}\right|-{E}\right)$
104 102 67 66 addassd ${⊢}{\phi }\to {E}+1+\left|{W}\right|={E}+1+\left|{W}\right|$
105 104 oveq1d ${⊢}{\phi }\to \left({E}+1\right)+\left|{W}\right|-{E}={E}+\left(1+\left|{W}\right|\right)-{E}$
106 96 103 105 3eqtr2d ${⊢}{\phi }\to \left|{U}\right|={E}+\left(1+\left|{W}\right|\right)-{E}$
107 67 66 addcld ${⊢}{\phi }\to 1+\left|{W}\right|\in ℂ$
108 102 107 pncan2d ${⊢}{\phi }\to {E}+\left(1+\left|{W}\right|\right)-{E}=1+\left|{W}\right|$
109 67 66 addcomd ${⊢}{\phi }\to 1+\left|{W}\right|=\left|{W}\right|+1$
110 106 108 109 3eqtrd ${⊢}{\phi }\to \left|{U}\right|=\left|{W}\right|+1$
111 66 67 110 mvrraddd ${⊢}{\phi }\to \left|{U}\right|-1=\left|{W}\right|$
112 111 oveq2d ${⊢}{\phi }\to \left(0..^\left|{U}\right|-1\right)=\left(0..^\left|{W}\right|\right)$
113 63 112 eleqtrrd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^\left|{U}\right|-1\right)$
114 1 3 46 47 113 cycpmfv1 ${⊢}{\phi }\to {M}\left({U}\right)\left({U}\left({{W}}^{-1}\left({J}\right)\right)\right)={U}\left({{W}}^{-1}\left({J}\right)+1\right)$
115 7 fveq2i ${⊢}{U}\left({E}\right)={U}\left({{W}}^{-1}\left({J}\right)+1\right)$
116 114 115 syl6eqr ${⊢}{\phi }\to {M}\left({U}\right)\left({U}\left({{W}}^{-1}\left({J}\right)\right)\right)={U}\left({E}\right)$
117 1 3 20 27 18 32 cycpmfv3 ${⊢}{\phi }\to {M}\left({W}\right)\left({I}\right)={I}$
118 56 116 117 3eqtr4d ${⊢}{\phi }\to {M}\left({U}\right)\left({U}\left({{W}}^{-1}\left({J}\right)\right)\right)={M}\left({W}\right)\left({I}\right)$
119 72 fveq1d ${⊢}{\phi }\to {U}\left({{W}}^{-1}\left({J}\right)\right)=\left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\left({{W}}^{-1}\left({J}\right)\right)$
120 fzossfzop1 ${⊢}{E}\in {ℕ}_{0}\to \left(0..^{E}\right)\subseteq \left(0..^{E}+1\right)$
121 98 120 syl ${⊢}{\phi }\to \left(0..^{E}\right)\subseteq \left(0..^{E}+1\right)$
122 elfzonn0 ${⊢}{{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\right|\right)\to {{W}}^{-1}\left({J}\right)\in {ℕ}_{0}$
123 fzonn0p1 ${⊢}{{W}}^{-1}\left({J}\right)\in {ℕ}_{0}\to {{W}}^{-1}\left({J}\right)\in \left(0..^{{W}}^{-1}\left({J}\right)+1\right)$
124 63 122 123 3syl ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^{{W}}^{-1}\left({J}\right)+1\right)$
125 7 oveq2i ${⊢}\left(0..^{E}\right)=\left(0..^{{W}}^{-1}\left({J}\right)+1\right)$
126 124 125 eleqtrrdi ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^{E}\right)$
127 121 126 sseldd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^{E}+1\right)$
128 90 oveq2d ${⊢}{\phi }\to \left(0..^\left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|\right)=\left(0..^{E}+1\right)$
129 127 128 eleqtrrd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^\left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|\right)$
130 ccatval1 ${⊢}\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\in \mathrm{Word}{D}\wedge {W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\in \mathrm{Word}{D}\wedge {{W}}^{-1}\left({J}\right)\in \left(0..^\left|\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right|\right)\right)\to \left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\left({{W}}^{-1}\left({J}\right)\right)=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\left({{W}}^{-1}\left({J}\right)\right)$
131 77 79 129 130 syl3anc ${⊢}{\phi }\to \left(\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\mathrm{++}\left({W}\mathrm{substr}⟨{E},\left|{W}\right|⟩\right)\right)\left({{W}}^{-1}\left({J}\right)\right)=\left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\left({{W}}^{-1}\left({J}\right)\right)$
132 88 oveq2d ${⊢}{\phi }\to \left(0..^\left|{W}\mathrm{prefix}{E}\right|\right)=\left(0..^{E}\right)$
133 126 132 eleqtrrd ${⊢}{\phi }\to {{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\mathrm{prefix}{E}\right|\right)$
134 ccatval1 ${⊢}\left({W}\mathrm{prefix}{E}\in \mathrm{Word}{D}\wedge ⟨“{I}”⟩\in \mathrm{Word}{D}\wedge {{W}}^{-1}\left({J}\right)\in \left(0..^\left|{W}\mathrm{prefix}{E}\right|\right)\right)\to \left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\left({{W}}^{-1}\left({J}\right)\right)=\left({W}\mathrm{prefix}{E}\right)\left({{W}}^{-1}\left({J}\right)\right)$
135 75 43 133 134 syl3anc ${⊢}{\phi }\to \left(\left({W}\mathrm{prefix}{E}\right)\mathrm{++}⟨“{I}”⟩\right)\left({{W}}^{-1}\left({J}\right)\right)=\left({W}\mathrm{prefix}{E}\right)\left({{W}}^{-1}\left({J}\right)\right)$
136 119 131 135 3eqtrd ${⊢}{\phi }\to {U}\left({{W}}^{-1}\left({J}\right)\right)=\left({W}\mathrm{prefix}{E}\right)\left({{W}}^{-1}\left({J}\right)\right)$
137 pfxfv ${⊢}\left({W}\in \mathrm{Word}{D}\wedge {E}\in \left(0\dots \left|{W}\right|\right)\wedge {{W}}^{-1}\left({J}\right)\in \left(0..^{E}\right)\right)\to \left({W}\mathrm{prefix}{E}\right)\left({{W}}^{-1}\left({J}\right)\right)={W}\left({{W}}^{-1}\left({J}\right)\right)$
138 20 86 126 137 syl3anc ${⊢}{\phi }\to \left({W}\mathrm{prefix}{E}\right)\left({{W}}^{-1}\left({J}\right)\right)={W}\left({{W}}^{-1}\left({J}\right)\right)$
139 f1f1orn ${⊢}{W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}\to {W}:\mathrm{dom}{W}\underset{1-1 onto}{⟶}\mathrm{ran}{W}$
140 27 139 syl ${⊢}{\phi }\to {W}:\mathrm{dom}{W}\underset{1-1 onto}{⟶}\mathrm{ran}{W}$
141 f1ocnvfv2 ${⊢}\left({W}:\mathrm{dom}{W}\underset{1-1 onto}{⟶}\mathrm{ran}{W}\wedge {J}\in \mathrm{ran}{W}\right)\to {W}\left({{W}}^{-1}\left({J}\right)\right)={J}$
142 140 6 141 syl2anc ${⊢}{\phi }\to {W}\left({{W}}^{-1}\left({J}\right)\right)={J}$
143 136 138 142 3eqtrd ${⊢}{\phi }\to {U}\left({{W}}^{-1}\left({J}\right)\right)={J}$
144 143 fveq2d ${⊢}{\phi }\to {M}\left({U}\right)\left({U}\left({{W}}^{-1}\left({J}\right)\right)\right)={M}\left({U}\right)\left({J}\right)$
145 55 118 144 3eqtr2d ${⊢}{\phi }\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)\right)={M}\left({U}\right)\left({J}\right)$
146 145 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)\right)={M}\left({U}\right)\left({J}\right)$
147 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {i}={J}$
148 147 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)={M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)$
149 148 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({J}\right)\right)$
150 147 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({U}\right)\left({J}\right)$
151 146 149 150 3eqtr4d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}={J}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
152 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {D}\in {V}$
153 18 31 s2cld ${⊢}{\phi }\to ⟨“{I}{J}”⟩\in \mathrm{Word}{D}$
154 153 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to ⟨“{I}{J}”⟩\in \mathrm{Word}{D}$
155 18 31 35 s2f1 ${⊢}{\phi }\to ⟨“{I}{J}”⟩:\mathrm{dom}⟨“{I}{J}”⟩\underset{1-1}{⟶}{D}$
156 155 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to ⟨“{I}{J}”⟩:\mathrm{dom}⟨“{I}{J}”⟩\underset{1-1}{⟶}{D}$
157 30 sselda ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {i}\in {D}$
158 157 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {i}\in {D}$
159 simpr ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {i}\in \mathrm{ran}{W}$
160 32 adantr ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to ¬{I}\in \mathrm{ran}{W}$
161 nelne2 ${⊢}\left({i}\in \mathrm{ran}{W}\wedge ¬{I}\in \mathrm{ran}{W}\right)\to {i}\ne {I}$
162 159 160 161 syl2anc ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {i}\ne {I}$
163 162 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {i}\ne {I}$
164 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {i}\ne {J}$
165 163 164 nelprd ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to ¬{i}\in \left\{{I},{J}\right\}$
166 18 31 s2rn ${⊢}{\phi }\to \mathrm{ran}⟨“{I}{J}”⟩=\left\{{I},{J}\right\}$
167 166 eleq2d ${⊢}{\phi }\to \left({i}\in \mathrm{ran}⟨“{I}{J}”⟩↔{i}\in \left\{{I},{J}\right\}\right)$
168 167 notbid ${⊢}{\phi }\to \left(¬{i}\in \mathrm{ran}⟨“{I}{J}”⟩↔¬{i}\in \left\{{I},{J}\right\}\right)$
169 168 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to \left(¬{i}\in \mathrm{ran}⟨“{I}{J}”⟩↔¬{i}\in \left\{{I},{J}\right\}\right)$
170 165 169 mpbird ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to ¬{i}\in \mathrm{ran}⟨“{I}{J}”⟩$
171 1 152 154 156 158 170 cycpmfv3 ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)={i}$
172 171 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({W}\right)\left({i}\right)$
173 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {D}\in {V}$
174 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {W}\in \mathrm{dom}{M}$
175 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {I}\in \left({D}\setminus \mathrm{ran}{W}\right)$
176 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {J}\in \mathrm{ran}{W}$
177 simpllr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {i}\in \mathrm{ran}{W}$
178 simplr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {i}\ne {J}$
179 simpr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)$
180 1 2 173 174 175 176 7 8 177 178 179 cycpmco2lem7 ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({W}\right)\left({i}\right)$
181 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {D}\in {V}$
182 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {W}\in \mathrm{dom}{M}$
183 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {I}\in \left({D}\setminus \mathrm{ran}{W}\right)$
184 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {J}\in \mathrm{ran}{W}$
185 simpllr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {i}\in \mathrm{ran}{W}$
186 162 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {i}\ne {I}$
187 simpr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)$
188 1 2 181 182 183 184 7 8 185 186 187 cycpmco2lem6 ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({W}\right)\left({i}\right)$
189 3 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {D}\in {V}$
190 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {W}\in \mathrm{dom}{M}$
191 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {I}\in \left({D}\setminus \mathrm{ran}{W}\right)$
192 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {J}\in \mathrm{ran}{W}$
193 simpllr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {i}\in \mathrm{ran}{W}$
194 simpr ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1$
195 1 2 189 190 191 192 7 8 193 194 cycpmco2lem5 ${⊢}\left(\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\wedge {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({W}\right)\left({i}\right)$
196 f1f1orn ${⊢}{U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}\to {U}:\mathrm{dom}{U}\underset{1-1 onto}{⟶}\mathrm{ran}{U}$
197 47 196 syl ${⊢}{\phi }\to {U}:\mathrm{dom}{U}\underset{1-1 onto}{⟶}\mathrm{ran}{U}$
198 ssun1 ${⊢}\mathrm{ran}{W}\subseteq \mathrm{ran}{W}\cup \left\{{I}\right\}$
199 1 2 3 4 5 6 7 8 cycpmco2rn ${⊢}{\phi }\to \mathrm{ran}{U}=\mathrm{ran}{W}\cup \left\{{I}\right\}$
200 198 199 sseqtrrid ${⊢}{\phi }\to \mathrm{ran}{W}\subseteq \mathrm{ran}{U}$
201 200 sselda ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {i}\in \mathrm{ran}{U}$
202 f1ocnvdm ${⊢}\left({U}:\mathrm{dom}{U}\underset{1-1 onto}{⟶}\mathrm{ran}{U}\wedge {i}\in \mathrm{ran}{U}\right)\to {{U}}^{-1}\left({i}\right)\in \mathrm{dom}{U}$
203 197 201 202 syl2an2r ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {{U}}^{-1}\left({i}\right)\in \mathrm{dom}{U}$
204 wrddm ${⊢}{U}\in \mathrm{Word}{D}\to \mathrm{dom}{U}=\left(0..^\left|{U}\right|\right)$
205 46 204 syl ${⊢}{\phi }\to \mathrm{dom}{U}=\left(0..^\left|{U}\right|\right)$
206 205 adantr ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \mathrm{dom}{U}=\left(0..^\left|{U}\right|\right)$
207 203 206 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|\right)$
208 65 nn0zd ${⊢}{\phi }\to \left|{W}\right|\in ℤ$
209 208 peano2zd ${⊢}{\phi }\to \left|{W}\right|+1\in ℤ$
210 110 209 eqeltrd ${⊢}{\phi }\to \left|{U}\right|\in ℤ$
211 fzoval ${⊢}\left|{U}\right|\in ℤ\to \left(0..^\left|{U}\right|\right)=\left(0\dots \left|{U}\right|-1\right)$
212 210 211 syl ${⊢}{\phi }\to \left(0..^\left|{U}\right|\right)=\left(0\dots \left|{U}\right|-1\right)$
213 212 adantr ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left(0..^\left|{U}\right|\right)=\left(0\dots \left|{U}\right|-1\right)$
214 207 213 eleqtrd ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {{U}}^{-1}\left({i}\right)\in \left(0\dots \left|{U}\right|-1\right)$
215 elfzr ${⊢}{{U}}^{-1}\left({i}\right)\in \left(0\dots \left|{U}\right|-1\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
216 214 215 syl ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
217 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\right)\to {{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)$
218 99 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\right)\to {E}\in ℤ$
219 fzospliti ${⊢}\left({{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\wedge {E}\in ℤ\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)$
220 217 218 219 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)$
221 220 ex ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\right)$
222 221 orim1d ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left(\left({{U}}^{-1}\left({i}\right)\in \left(0..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\to \left(\left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)\right)$
223 216 222 mpd ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left(\left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
224 df-3or ${⊢}\left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)↔\left(\left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
225 223 224 sylibr ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
226 225 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to \left({{U}}^{-1}\left({i}\right)\in \left(0..^{E}\right)\vee {{U}}^{-1}\left({i}\right)\in \left({E}..^\left|{U}\right|-1\right)\vee {{U}}^{-1}\left({i}\right)=\left|{U}\right|-1\right)$
227 180 188 195 226 mpjao3dan ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({W}\right)\left({i}\right)$
228 172 227 eqtr4d ${⊢}\left(\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\wedge {i}\ne {J}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
229 151 228 pm2.61dane ${⊢}\left({\phi }\wedge {i}\in \mathrm{ran}{W}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
230 229 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in {D}\right)\wedge {i}\in \mathrm{ran}{W}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
231 1 2 3 4 5 6 7 8 cycpmco2lem4 ${⊢}{\phi }\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({I}\right)\right)={M}\left({U}\right)\left({I}\right)$
232 231 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({I}\right)\right)={M}\left({U}\right)\left({I}\right)$
233 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {i}={I}$
234 233 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)={M}\left(⟨“{I}{J}”⟩\right)\left({I}\right)$
235 234 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({I}\right)\right)$
236 233 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {M}\left({U}\right)\left({i}\right)={M}\left({U}\right)\left({I}\right)$
237 232 235 236 3eqtr4d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}={I}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
238 3 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {D}\in {V}$
239 20 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {W}\in \mathrm{Word}{D}$
240 27 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {W}:\mathrm{dom}{W}\underset{1-1}{⟶}{D}$
241 simplr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {i}\in \left({D}\setminus \mathrm{ran}{W}\right)$
242 241 eldifad ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {i}\in {D}$
243 241 eldifbd ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ¬{i}\in \mathrm{ran}{W}$
244 1 238 239 240 242 243 cycpmfv3 ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {M}\left({W}\right)\left({i}\right)={i}$
245 153 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ⟨“{I}{J}”⟩\in \mathrm{Word}{D}$
246 155 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ⟨“{I}{J}”⟩:\mathrm{dom}⟨“{I}{J}”⟩\underset{1-1}{⟶}{D}$
247 simpr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {i}\ne {I}$
248 eldifn ${⊢}{i}\in \left({D}\setminus \mathrm{ran}{W}\right)\to ¬{i}\in \mathrm{ran}{W}$
249 nelne2 ${⊢}\left({J}\in \mathrm{ran}{W}\wedge ¬{i}\in \mathrm{ran}{W}\right)\to {J}\ne {i}$
250 6 248 249 syl2an ${⊢}\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\to {J}\ne {i}$
251 250 necomd ${⊢}\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\to {i}\ne {J}$
252 251 adantr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {i}\ne {J}$
253 247 252 nelprd ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ¬{i}\in \left\{{I},{J}\right\}$
254 168 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to \left(¬{i}\in \mathrm{ran}⟨“{I}{J}”⟩↔¬{i}\in \left\{{I},{J}\right\}\right)$
255 253 254 mpbird ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ¬{i}\in \mathrm{ran}⟨“{I}{J}”⟩$
256 1 238 245 246 242 255 cycpmfv3 ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)={i}$
257 256 fveq2d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({W}\right)\left({i}\right)$
258 46 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {U}\in \mathrm{Word}{D}$
259 47 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {U}:\mathrm{dom}{U}\underset{1-1}{⟶}{D}$
260 199 ad2antrr ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to \mathrm{ran}{U}=\mathrm{ran}{W}\cup \left\{{I}\right\}$
261 nelsn ${⊢}{i}\ne {I}\to ¬{i}\in \left\{{I}\right\}$
262 261 adantl ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ¬{i}\in \left\{{I}\right\}$
263 nelun ${⊢}\mathrm{ran}{U}=\mathrm{ran}{W}\cup \left\{{I}\right\}\to \left(¬{i}\in \mathrm{ran}{U}↔\left(¬{i}\in \mathrm{ran}{W}\wedge ¬{i}\in \left\{{I}\right\}\right)\right)$
264 263 biimpar ${⊢}\left(\mathrm{ran}{U}=\mathrm{ran}{W}\cup \left\{{I}\right\}\wedge \left(¬{i}\in \mathrm{ran}{W}\wedge ¬{i}\in \left\{{I}\right\}\right)\right)\to ¬{i}\in \mathrm{ran}{U}$
265 260 243 262 264 syl12anc ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to ¬{i}\in \mathrm{ran}{U}$
266 1 238 258 259 242 265 cycpmfv3 ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {M}\left({U}\right)\left({i}\right)={i}$
267 244 257 266 3eqtr4d ${⊢}\left(\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\wedge {i}\ne {I}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
268 237 267 pm2.61dane ${⊢}\left({\phi }\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
269 268 adantlr ${⊢}\left(\left({\phi }\wedge {i}\in {D}\right)\wedge {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
270 elun ${⊢}{i}\in \left(\mathrm{ran}{W}\cup \left({D}\setminus \mathrm{ran}{W}\right)\right)↔\left({i}\in \mathrm{ran}{W}\vee {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)$
271 undif ${⊢}\mathrm{ran}{W}\subseteq {D}↔\mathrm{ran}{W}\cup \left({D}\setminus \mathrm{ran}{W}\right)={D}$
272 30 271 sylib ${⊢}{\phi }\to \mathrm{ran}{W}\cup \left({D}\setminus \mathrm{ran}{W}\right)={D}$
273 272 eleq2d ${⊢}{\phi }\to \left({i}\in \left(\mathrm{ran}{W}\cup \left({D}\setminus \mathrm{ran}{W}\right)\right)↔{i}\in {D}\right)$
274 270 273 syl5rbbr ${⊢}{\phi }\to \left({i}\in {D}↔\left({i}\in \mathrm{ran}{W}\vee {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)\right)$
275 274 biimpa ${⊢}\left({\phi }\wedge {i}\in {D}\right)\to \left({i}\in \mathrm{ran}{W}\vee {i}\in \left({D}\setminus \mathrm{ran}{W}\right)\right)$
276 230 269 275 mpjaodan ${⊢}\left({\phi }\wedge {i}\in {D}\right)\to {M}\left({W}\right)\left({M}\left(⟨“{I}{J}”⟩\right)\left({i}\right)\right)={M}\left({U}\right)\left({i}\right)$
277 53 276 eqtrd ${⊢}\left({\phi }\wedge {i}\in {D}\right)\to \left({M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)\right)\left({i}\right)={M}\left({U}\right)\left({i}\right)$
278 42 51 277 eqfnfvd ${⊢}{\phi }\to {M}\left({W}\right)\circ {M}\left(⟨“{I}{J}”⟩\right)={M}\left({U}\right)$