Metamath Proof Explorer


Theorem cycpmco2lem5

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c 𝑀 = ( toCyc ‘ 𝐷 )
cycpmco2.s 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmco2.d ( 𝜑𝐷𝑉 )
cycpmco2.w ( 𝜑𝑊 ∈ dom 𝑀 )
cycpmco2.i ( 𝜑𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
cycpmco2.j ( 𝜑𝐽 ∈ ran 𝑊 )
cycpmco2.e 𝐸 = ( ( 𝑊𝐽 ) + 1 )
cycpmco2.1 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
cycpmco2lem.1 ( 𝜑𝐾 ∈ ran 𝑊 )
cycpmco2lem5.1 ( 𝜑 → ( 𝑈𝐾 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
Assertion cycpmco2lem5 ( 𝜑 → ( ( 𝑀𝑈 ) ‘ 𝐾 ) = ( ( 𝑀𝑊 ) ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cycpmco2.c 𝑀 = ( toCyc ‘ 𝐷 )
2 cycpmco2.s 𝑆 = ( SymGrp ‘ 𝐷 )
3 cycpmco2.d ( 𝜑𝐷𝑉 )
4 cycpmco2.w ( 𝜑𝑊 ∈ dom 𝑀 )
5 cycpmco2.i ( 𝜑𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) )
6 cycpmco2.j ( 𝜑𝐽 ∈ ran 𝑊 )
7 cycpmco2.e 𝐸 = ( ( 𝑊𝐽 ) + 1 )
8 cycpmco2.1 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
9 cycpmco2lem.1 ( 𝜑𝐾 ∈ ran 𝑊 )
10 cycpmco2lem5.1 ( 𝜑 → ( 𝑈𝐾 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
11 9 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → 𝐾 ∈ ran 𝑊 )
12 ovexd ( 𝜑 → ( ( 𝑊𝐽 ) + 1 ) ∈ V )
13 7 12 eqeltrid ( 𝜑𝐸 ∈ V )
14 5 eldifad ( 𝜑𝐼𝐷 )
15 14 s1cld ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
16 splval ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
17 4 13 13 15 16 syl13anc ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
18 8 17 syl5eq ( 𝜑𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
19 18 fveq2d ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
20 ssrab2 { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ⊆ Word 𝐷
21 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
22 1 2 21 tocycf ( 𝐷𝑉𝑀 : { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ⟶ ( Base ‘ 𝑆 ) )
23 3 22 syl ( 𝜑𝑀 : { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ⟶ ( Base ‘ 𝑆 ) )
24 23 fdmd ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } )
25 4 24 eleqtrd ( 𝜑𝑊 ∈ { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } )
26 20 25 sselid ( 𝜑𝑊 ∈ Word 𝐷 )
27 pfxcl ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
28 26 27 syl ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
29 ccatcl ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
30 28 15 29 syl2anc ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
31 swrdcl ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
32 26 31 syl ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
33 ccatlen ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ) → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
34 30 32 33 syl2anc ( 𝜑 → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
35 ccatws1len ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
36 28 35 syl ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
37 id ( 𝑤 = 𝑊𝑤 = 𝑊 )
38 dmeq ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
39 eqidd ( 𝑤 = 𝑊𝐷 = 𝐷 )
40 37 38 39 f1eq123d ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤1-1𝐷𝑊 : dom 𝑊1-1𝐷 ) )
41 40 elrab ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷𝑤 : dom 𝑤1-1𝐷 } ↔ ( 𝑊 ∈ Word 𝐷𝑊 : dom 𝑊1-1𝐷 ) )
42 25 41 sylib ( 𝜑 → ( 𝑊 ∈ Word 𝐷𝑊 : dom 𝑊1-1𝐷 ) )
43 42 simprd ( 𝜑𝑊 : dom 𝑊1-1𝐷 )
44 f1cnv ( 𝑊 : dom 𝑊1-1𝐷 𝑊 : ran 𝑊1-1-onto→ dom 𝑊 )
45 43 44 syl ( 𝜑 𝑊 : ran 𝑊1-1-onto→ dom 𝑊 )
46 f1of ( 𝑊 : ran 𝑊1-1-onto→ dom 𝑊 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
47 45 46 syl ( 𝜑 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
48 47 6 ffvelrnd ( 𝜑 → ( 𝑊𝐽 ) ∈ dom 𝑊 )
49 wrddm ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
50 26 49 syl ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
51 48 50 eleqtrd ( 𝜑 → ( 𝑊𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
52 fzofzp1 ( ( 𝑊𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
53 51 52 syl ( 𝜑 → ( ( 𝑊𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
54 7 53 eqeltrid ( 𝜑𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
55 pfxlen ( ( 𝑊 ∈ Word 𝐷𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
56 26 54 55 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
57 56 oveq1d ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) )
58 36 57 eqtrd ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
59 lencl ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
60 26 59 syl ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
61 nn0fz0 ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
62 60 61 sylib ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
63 swrdlen ( ( 𝑊 ∈ Word 𝐷𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
64 26 54 62 63 syl3anc ( 𝜑 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
65 58 64 oveq12d ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
66 19 34 65 3eqtrd ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
67 fz0ssnn0 ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
68 67 54 sselid ( 𝜑𝐸 ∈ ℕ0 )
69 68 nn0zd ( 𝜑𝐸 ∈ ℤ )
70 69 peano2zd ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ )
71 70 zcnd ( 𝜑 → ( 𝐸 + 1 ) ∈ ℂ )
72 60 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
73 68 nn0cnd ( 𝜑𝐸 ∈ ℂ )
74 71 72 73 addsubassd ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
75 1cnd ( 𝜑 → 1 ∈ ℂ )
76 73 75 72 addassd ( 𝜑 → ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) = ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) )
77 76 oveq1d ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
78 66 74 77 3eqtr2d ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
79 75 72 addcld ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
80 73 79 pncan2d ( 𝜑 → ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) = ( 1 + ( ♯ ‘ 𝑊 ) ) )
81 75 72 addcomd ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
82 78 80 81 3eqtrd ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
83 oveq1 ( ( ♯ ‘ 𝑊 ) = 𝐸 → ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝐸 + 1 ) )
84 82 83 sylan9eq ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ♯ ‘ 𝑈 ) = ( 𝐸 + 1 ) )
85 84 oveq1d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( 𝐸 + 1 ) − 1 ) )
86 73 75 pncand ( 𝜑 → ( ( 𝐸 + 1 ) − 1 ) = 𝐸 )
87 86 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( 𝐸 + 1 ) − 1 ) = 𝐸 )
88 85 87 eqtrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = 𝐸 )
89 88 fveq2d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 𝑈𝐸 ) )
90 10 fveq2d ( 𝜑 → ( 𝑈 ‘ ( 𝑈𝐾 ) ) = ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
91 1 2 3 4 5 6 7 8 cycpmco2f1 ( 𝜑𝑈 : dom 𝑈1-1𝐷 )
92 f1f1orn ( 𝑈 : dom 𝑈1-1𝐷𝑈 : dom 𝑈1-1-onto→ ran 𝑈 )
93 91 92 syl ( 𝜑𝑈 : dom 𝑈1-1-onto→ ran 𝑈 )
94 ssun1 ran 𝑊 ⊆ ( ran 𝑊 ∪ { 𝐼 } )
95 1 2 3 4 5 6 7 8 cycpmco2rn ( 𝜑 → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) )
96 94 95 sseqtrrid ( 𝜑 → ran 𝑊 ⊆ ran 𝑈 )
97 96 sselda ( ( 𝜑𝐾 ∈ ran 𝑊 ) → 𝐾 ∈ ran 𝑈 )
98 f1ocnvfv2 ( ( 𝑈 : dom 𝑈1-1-onto→ ran 𝑈𝐾 ∈ ran 𝑈 ) → ( 𝑈 ‘ ( 𝑈𝐾 ) ) = 𝐾 )
99 93 97 98 syl2an2r ( ( 𝜑𝐾 ∈ ran 𝑊 ) → ( 𝑈 ‘ ( 𝑈𝐾 ) ) = 𝐾 )
100 9 99 mpdan ( 𝜑 → ( 𝑈 ‘ ( 𝑈𝐾 ) ) = 𝐾 )
101 90 100 eqtr3d ( 𝜑 → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = 𝐾 )
102 101 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = 𝐾 )
103 1 2 3 4 5 6 7 8 cycpmco2lem2 ( 𝜑 → ( 𝑈𝐸 ) = 𝐼 )
104 103 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( 𝑈𝐸 ) = 𝐼 )
105 89 102 104 3eqtr3d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → 𝐾 = 𝐼 )
106 5 eldifbd ( 𝜑 → ¬ 𝐼 ∈ ran 𝑊 )
107 106 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ¬ 𝐼 ∈ ran 𝑊 )
108 105 107 eqneltrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ¬ 𝐾 ∈ ran 𝑊 )
109 11 108 pm2.21dd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) = 𝐸 ) → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
110 splcl ( ( 𝑊 ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
111 26 15 110 syl2anc ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
112 8 111 eqeltrid ( 𝜑𝑈 ∈ Word 𝐷 )
113 nn0p1gt0 ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
114 60 113 syl ( 𝜑 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
115 114 82 breqtrrd ( 𝜑 → 0 < ( ♯ ‘ 𝑈 ) )
116 eqidd ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ♯ ‘ 𝑈 ) − 1 ) )
117 1 3 112 91 115 116 cycpmfv2 ( 𝜑 → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( 𝑈 ‘ 0 ) )
118 117 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( 𝑈 ‘ 0 ) )
119 f1f ( 𝑊 : dom 𝑊1-1𝐷𝑊 : dom 𝑊𝐷 )
120 43 119 syl ( 𝜑𝑊 : dom 𝑊𝐷 )
121 120 frnd ( 𝜑 → ran 𝑊𝐷 )
122 3 121 ssexd ( 𝜑 → ran 𝑊 ∈ V )
123 6 ne0d ( 𝜑 → ran 𝑊 ≠ ∅ )
124 hashgt0 ( ( ran 𝑊 ∈ V ∧ ran 𝑊 ≠ ∅ ) → 0 < ( ♯ ‘ ran 𝑊 ) )
125 122 123 124 syl2anc ( 𝜑 → 0 < ( ♯ ‘ ran 𝑊 ) )
126 4 dmexd ( 𝜑 → dom 𝑊 ∈ V )
127 hashf1rn ( ( dom 𝑊 ∈ V ∧ 𝑊 : dom 𝑊1-1𝐷 ) → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ran 𝑊 ) )
128 126 43 127 syl2anc ( 𝜑 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ ran 𝑊 ) )
129 125 128 breqtrrd ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) )
130 eqidd ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
131 1 3 26 43 129 130 cycpmfv2 ( 𝜑 → ( ( 𝑀𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ 0 ) )
132 131 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) = ( 𝑊 ‘ 0 ) )
133 8 a1i ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) )
134 1 2 3 4 5 6 7 8 cycpmco2lem3 ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
135 73 75 addcomd ( 𝜑 → ( 𝐸 + 1 ) = ( 1 + 𝐸 ) )
136 135 oveq2d ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) )
137 72 75 subcld ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℂ )
138 137 73 75 nppcan3d ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) )
139 72 75 npcand ( 𝜑 → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
140 136 138 139 3eqtrd ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) = ( ♯ ‘ 𝑊 ) )
141 134 140 eqtr4d ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) )
142 141 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) )
143 133 142 fveq12d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) )
144 26 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝑊 ∈ Word 𝐷 )
145 nn0fz0 ( 𝐸 ∈ ℕ0𝐸 ∈ ( 0 ... 𝐸 ) )
146 68 145 sylib ( 𝜑𝐸 ∈ ( 0 ... 𝐸 ) )
147 146 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ( 0 ... 𝐸 ) )
148 54 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
149 15 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
150 72 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
151 1cnd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 1 ∈ ℂ )
152 73 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → 𝐸 ∈ ℂ )
153 150 151 152 sub32d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) = ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) )
154 fznn0sub ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 )
155 54 154 syl ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 )
156 155 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ0 )
157 simpr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ♯ ‘ 𝑊 ) ≠ 𝐸 )
158 150 152 156 157 subne0nn ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ )
159 fzo0end ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℕ → ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
160 158 159 syl ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
161 153 160 eqeltrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
162 s1len ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) = 1
163 162 eqcomi 1 = ( ♯ ‘ ⟨“ 𝐼 ”⟩ )
164 163 oveq2i ( 𝐸 + 1 ) = ( 𝐸 + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) )
165 164 a1i ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝐸 + 1 ) = ( 𝐸 + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) )
166 144 147 148 149 161 165 splfv3 ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + ( 𝐸 + 1 ) ) ) = ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) )
167 137 73 npcand ( 𝜑 → ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
168 167 fveq2d ( 𝜑 → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
169 168 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑊 ‘ ( ( ( ( ♯ ‘ 𝑊 ) − 1 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
170 143 166 169 3eqtrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
171 170 fveq2d ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑊 ) ‘ ( 𝑊 ‘ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) )
172 18 fveq1d ( 𝜑 → ( 𝑈 ‘ 0 ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) )
173 nn0p1nn ( 𝐸 ∈ ℕ0 → ( 𝐸 + 1 ) ∈ ℕ )
174 68 173 syl ( 𝜑 → ( 𝐸 + 1 ) ∈ ℕ )
175 lbfzo0 ( 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) ↔ ( 𝐸 + 1 ) ∈ ℕ )
176 174 175 sylibr ( 𝜑 → 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
177 58 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = ( 0 ..^ ( 𝐸 + 1 ) ) )
178 176 177 eleqtrrd ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) )
179 ccatval1 ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) )
180 30 32 178 179 syl3anc ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) )
181 elfzonn0 ( ( 𝑊𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑊𝐽 ) ∈ ℕ0 )
182 51 181 syl ( 𝜑 → ( 𝑊𝐽 ) ∈ ℕ0 )
183 nn0p1nn ( ( 𝑊𝐽 ) ∈ ℕ0 → ( ( 𝑊𝐽 ) + 1 ) ∈ ℕ )
184 182 183 syl ( 𝜑 → ( ( 𝑊𝐽 ) + 1 ) ∈ ℕ )
185 7 184 eqeltrid ( 𝜑𝐸 ∈ ℕ )
186 lbfzo0 ( 0 ∈ ( 0 ..^ 𝐸 ) ↔ 𝐸 ∈ ℕ )
187 185 186 sylibr ( 𝜑 → 0 ∈ ( 0 ..^ 𝐸 ) )
188 56 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = ( 0 ..^ 𝐸 ) )
189 187 188 eleqtrrd ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) )
190 ccatval1 ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) )
191 28 15 189 190 syl3anc ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) )
192 nn0p1gt0 ( ( 𝑊𝐽 ) ∈ ℕ0 → 0 < ( ( 𝑊𝐽 ) + 1 ) )
193 182 192 syl ( 𝜑 → 0 < ( ( 𝑊𝐽 ) + 1 ) )
194 193 7 breqtrrdi ( 𝜑 → 0 < 𝐸 )
195 194 gt0ne0d ( 𝜑𝐸 ≠ 0 )
196 fzne1 ( ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐸 ≠ 0 ) → 𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) )
197 54 195 196 syl2anc ( 𝜑𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) )
198 0p1e1 ( 0 + 1 ) = 1
199 198 oveq1i ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ♯ ‘ 𝑊 ) )
200 197 199 eleqtrdi ( 𝜑𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
201 pfxfv0 ( ( 𝑊 ∈ Word 𝐷𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
202 26 200 201 syl2anc ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
203 180 191 202 3eqtrd ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
204 172 203 eqtrd ( 𝜑 → ( 𝑈 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
205 204 adantr ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ 0 ) = ( 𝑊 ‘ 0 ) )
206 132 171 205 3eqtr4rd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( 𝑈 ‘ 0 ) = ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
207 118 206 eqtrd ( ( 𝜑 ∧ ( ♯ ‘ 𝑊 ) ≠ 𝐸 ) → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
208 109 207 pm2.61dane ( 𝜑 → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) )
209 101 fveq2d ( 𝜑 → ( ( 𝑀𝑈 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑈 ) ‘ 𝐾 ) )
210 101 fveq2d ( 𝜑 → ( ( 𝑀𝑊 ) ‘ ( 𝑈 ‘ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ) = ( ( 𝑀𝑊 ) ‘ 𝐾 ) )
211 208 209 210 3eqtr3d ( 𝜑 → ( ( 𝑀𝑈 ) ‘ 𝐾 ) = ( ( 𝑀𝑊 ) ‘ 𝐾 ) )