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 eqtrid ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 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 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ 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 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )