Metamath Proof Explorer

Theorem cycpmco2lem4

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 ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
Assertion cycpmco2lem4 ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )

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 1 2 3 4 5 6 7 8 cycpmco2lem1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐷 ∈ 𝑉 )
11 ssrab2 ⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
12 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13 1 2 12 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
14 3 13 syl ⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
15 14 fdmd ⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
16 4 15 eleqtrd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
17 11 16 sselid ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
18 5 eldifad ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
19 18 s1cld ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
20 splcl ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
21 17 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
22 8 21 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ Word 𝐷 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑈 ∈ Word 𝐷 )
24 1 2 3 4 5 6 7 8 cycpmco2f1 ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
27 1 2 3 4 5 6 7 8 cycpmco2lem3 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
28 27 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 26 29 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐸 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
31 1 10 23 25 30 cycpmfv1 ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( 𝑈 ‘ ( 𝐸 + 1 ) ) )
32 1 2 3 4 5 6 7 8 cycpmco2lem2 ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 )
33 32 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
35 17 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 ∈ Word 𝐷 )
36 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
37 17 36 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
38 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
39 37 38 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
41 swrdfv0 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 0 ) = ( 𝑊 ‘ 𝐸 ) )
42 35 26 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 0 ) = ( 𝑊 ‘ 𝐸 ) )
43 ovexd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V )
44 7 43 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ V )
45 splval ⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
46 4 44 44 19 45 syl13anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
47 8 46 syl5eq ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
48 47 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ ( 𝐸 + 1 ) ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( 𝐸 + 1 ) ) )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 ‘ ( 𝐸 + 1 ) ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( 𝐸 + 1 ) ) )
50 pfxcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
51 17 50 syl ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
52 ccatcl ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
53 51 19 52 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
55 swrdcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
56 17 55 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
58 1z ⊢ 1 ∈ ℤ
59 fzoaddel ⊢ ( ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 1 ∈ ℤ ) → ( 𝐸 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
60 58 59 mpan2 ⊢ ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐸 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
61 elfzolt2b ⊢ ( ( 𝐸 + 1 ) ∈ ( ( 0 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝐸 + 1 ) ∈ ( ( 𝐸 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
62 60 61 syl ⊢ ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐸 + 1 ) ∈ ( ( 𝐸 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
63 62 adantl ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐸 + 1 ) ∈ ( ( 𝐸 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
64 ccatws1len ⊢ ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
65 51 64 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
66 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
67 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
68 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
69 66 67 68 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
70 69 elrab3 ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
71 70 biimpa ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
72 17 16 71 syl2anc ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
73 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
74 72 73 syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
75 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
76 74 75 syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
77 76 6 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
78 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
79 17 78 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
80 77 79 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
81 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
82 80 81 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
83 7 82 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
84 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
85 17 83 84 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
86 85 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) )
87 65 86 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
89 47 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
90 ccatlen ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ) → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
91 53 56 90 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
92 swrdlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
93 17 83 39 92 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
94 87 93 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
95 89 91 94 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
96 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
97 96 83 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
98 97 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
99 98 peano2zd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ )
100 99 zcnd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℂ )
101 37 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
102 97 nn0cnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
103 100 101 102 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
104 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
105 102 104 101 addassd ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) = ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) )
106 105 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
107 95 103 106 3eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
108 104 101 addcld ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
109 102 108 pncan2d ⊢ ( 𝜑 → ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) = ( 1 + ( ♯ ‘ 𝑊 ) ) )
110 104 101 addcomd ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
111 107 109 110 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
112 89 111 91 3eqtr3rd ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
114 88 113 oveq12d ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ..^ ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) = ( ( 𝐸 + 1 ) ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
115 63 114 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐸 + 1 ) ∈ ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ..^ ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) )
116 ccatval2 ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ∧ ( 𝐸 + 1 ) ∈ ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ..^ ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( 𝐸 + 1 ) ) = ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) )
117 54 57 115 116 syl3anc ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ ( 𝐸 + 1 ) ) = ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) )
118 87 oveq2d ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = ( ( 𝐸 + 1 ) − ( 𝐸 + 1 ) ) )
119 100 subidd ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) − ( 𝐸 + 1 ) ) = 0 )
120 118 119 eqtrd ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = 0 )
121 120 fveq2d ⊢ ( 𝜑 → ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) = ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 0 ) )
122 121 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ ( ( 𝐸 + 1 ) − ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) = ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 0 ) )
123 49 117 122 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 ‘ ( 𝐸 + 1 ) ) = ( ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ‘ 0 ) )
124 7 fveq2i ⊢ ( 𝑊 ‘ 𝐸 ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
125 124 a1i ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 ‘ 𝐸 ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) )
126 72 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
127 7 oveq1i ⊢ ( 𝐸 − 1 ) = ( ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) − 1 )
128 elfzonn0 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
129 80 128 syl ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
130 129 nn0cnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℂ )
131 130 104 pncand ⊢ ( 𝜑 → ( ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) − 1 ) = ( ◡ 𝑊 ‘ 𝐽 ) )
132 127 131 eqtr2id ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) = ( 𝐸 − 1 ) )
133 132 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ◡ 𝑊 ‘ 𝐽 ) = ( 𝐸 − 1 ) )
134 nn0p1gt0 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → 0 < ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
135 129 134 syl ⊢ ( 𝜑 → 0 < ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
136 135 7 breqtrrdi ⊢ ( 𝜑 → 0 < 𝐸 )
137 136 gt0ne0d ⊢ ( 𝜑 → 𝐸 ≠ 0 )
138 137 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐸 ≠ 0 )
139 fzo1fzo0n0 ⊢ ( 𝐸 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) ↔ ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐸 ≠ 0 ) )
140 26 138 139 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → 𝐸 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) )
141 elfzo1elm1fzo0 ⊢ ( 𝐸 ∈ ( 1 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝐸 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
142 140 141 syl ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝐸 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
143 133 142 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
144 1 10 35 126 143 cycpmfv1 ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ) )
145 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
146 72 145 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
147 f1ocnvfv2 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝐽 ∈ ran 𝑊 ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
148 146 6 147 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
149 148 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )
150 149 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )
151 125 144 150 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) = ( 𝑊 ‘ 𝐸 ) )
152 42 123 151 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑈 ‘ ( 𝐸 + 1 ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )
153 31 34 152 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
154 149 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) )
155 3 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝐷 ∈ 𝑉 )
156 17 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝐷 )
157 72 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
158 136 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 0 < 𝐸 )
159 simpr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝐸 = ( ♯ ‘ 𝑊 ) )
160 158 159 breqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑊 ) )
161 oveq1 ⊢ ( 𝐸 = ( ♯ ‘ 𝑊 ) → ( 𝐸 − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
162 132 161 sylan9eq ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
163 1 155 156 157 160 162 cycpmfv2 ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) ) = ( 𝑊 ‘ 0 ) )
164 154 163 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) = ( 𝑊 ‘ 0 ) )
165 22 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝑈 ∈ Word 𝐷 )
166 24 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
167 nn0p1gt0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
168 37 167 syl ⊢ ( 𝜑 → 0 < ( ( ♯ ‘ 𝑊 ) + 1 ) )
169 168 111 breqtrrd ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑈 ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 0 < ( ♯ ‘ 𝑈 ) )
171 27 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
172 159 171 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → 𝐸 = ( ( ♯ ‘ 𝑈 ) − 1 ) )
173 1 155 165 166 170 172 cycpmfv2 ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( 𝑈 ‘ 0 ) )
174 47 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ 0 ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) )
175 174 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( 𝑈 ‘ 0 ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) )
176 nn0p1nn ⊢ ( 𝐸 ∈ ℕ0 → ( 𝐸 + 1 ) ∈ ℕ )
177 97 176 syl ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℕ )
178 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) ↔ ( 𝐸 + 1 ) ∈ ℕ )
179 177 178 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
180 87 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = ( 0 ..^ ( 𝐸 + 1 ) ) )
181 179 180 eleqtrrd ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) )
182 ccatval1 ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) )
183 53 56 181 182 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) )
184 nn0p1nn ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
185 129 184 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
186 7 185 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
187 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ 𝐸 ) ↔ 𝐸 ∈ ℕ )
188 186 187 sylibr ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ 𝐸 ) )
189 85 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = ( 0 ..^ 𝐸 ) )
190 188 189 eleqtrrd ⊢ ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) )
191 ccatval1 ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) )
192 51 19 190 191 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 0 ) = ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) )
193 fzne1 ⊢ ( ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐸 ≠ 0 ) → 𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) )
194 83 137 193 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) )
195 0p1e1 ⊢ ( 0 + 1 ) = 1
196 195 oveq1i ⊢ ( ( 0 + 1 ) ... ( ♯ ‘ 𝑊 ) ) = ( 1 ... ( ♯ ‘ 𝑊 ) )
197 194 196 eleqtrdi ⊢ ( 𝜑 → 𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
198 pfxfv0 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
199 17 197 198 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
200 183 192 199 3eqtrd ⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
201 200 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 0 ) = ( 𝑊 ‘ 0 ) )
202 173 175 201 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( 𝑊 ‘ 0 ) )
203 33 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ 𝐸 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
204 164 202 203 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝐸 = ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
205 elfzr ⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∨ 𝐸 = ( ♯ ‘ 𝑊 ) ) )
206 83 205 syl ⊢ ( 𝜑 → ( 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∨ 𝐸 = ( ♯ ‘ 𝑊 ) ) )
207 153 204 206 mpjaodan ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐽 ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )
208 9 207 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( ( 𝑀 ‘ ⟨“ 𝐼 𝐽 ”⟩ ) ‘ 𝐼 ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐼 ) )