Metamath Proof Explorer

Theorem cycpmco2lem7

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 ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ )
cycpmco2lem7.1 ⊢ ( 𝜑 → 𝐾 ∈ ran 𝑊 )
cycpmco2lem7.2 ⊢ ( 𝜑 → 𝐾 ≠ 𝐽 )
cycpmco2lem7.3 ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ 𝐸 ) )
Assertion cycpmco2lem7 ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )

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 cycpmco2lem7.1 ⊢ ( 𝜑 → 𝐾 ∈ ran 𝑊 )
10 cycpmco2lem7.2 ⊢ ( 𝜑 → 𝐾 ≠ 𝐽 )
11 cycpmco2lem7.3 ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ 𝐸 ) )
12 ssrab2 ⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
13 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 1 2 13 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
15 3 14 syl ⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
16 15 fdmd ⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
17 4 16 eleqtrd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
18 12 17 sseldi ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
19 5 eldifad ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
20 19 s1cld ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
21 splcl ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
22 18 20 21 syl2anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ∈ Word 𝐷 )
23 8 22 eqeltrid ⊢ ( 𝜑 → 𝑈 ∈ Word 𝐷 )
24 1 2 3 4 5 6 7 8 cycpmco2f1 ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1→ 𝐷 )
25 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
26 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
27 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
28 25 26 27 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
29 28 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
30 17 29 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
31 30 simprd ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
32 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
33 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
34 31 32 33 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
35 34 6 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
36 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
37 18 36 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 35 37 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
40 38 39 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
41 7 40 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
42 elfzuz3 ⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐸 ) )
43 fzoss2 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ 𝐸 ) → ( 0 ..^ 𝐸 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
44 41 42 43 3syl ⊢ ( 𝜑 → ( 0 ..^ 𝐸 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
45 1 2 3 4 5 6 7 8 cycpmco2lem3 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
46 45 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
47 44 46 sseqtrrd ⊢ ( 𝜑 → ( 0 ..^ 𝐸 ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
48 47 11 sseldd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
49 1 3 23 24 48 cycpmfv1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( 𝑈 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) ) )
50 f1f1orn ⊢ ( 𝑈 : dom 𝑈 –1-1→ 𝐷 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 )
51 24 50 syl ⊢ ( 𝜑 → 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 )
52 ssun1 ⊢ ran 𝑊 ⊆ ( ran 𝑊 ∪ { 𝐼 } )
53 1 2 3 4 5 6 7 8 cycpmco2rn ⊢ ( 𝜑 → ran 𝑈 = ( ran 𝑊 ∪ { 𝐼 } ) )
54 52 53 sseqtrrid ⊢ ( 𝜑 → ran 𝑊 ⊆ ran 𝑈 )
55 54 sselda ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → 𝐾 ∈ ran 𝑈 )
56 f1ocnvfv2 ⊢ ( ( 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ∧ 𝐾 ∈ ran 𝑈 ) → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 )
57 51 55 56 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 )
58 57 fveq2d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) )
59 9 58 mpdan ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) )
60 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
61 31 60 syl ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
62 44 37 sseqtrrd ⊢ ( 𝜑 → ( 0 ..^ 𝐸 ) ⊆ dom 𝑊 )
63 62 11 sseldd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑊 )
64 f1ocnvfv1 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑊 ) → ( ◡ 𝑊 ‘ ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ◡ 𝑈 ‘ 𝐾 ) )
65 61 63 64 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ◡ 𝑈 ‘ 𝐾 ) )
66 8 fveq1i ⊢ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ◡ 𝑈 ‘ 𝐾 ) )
67 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
68 67 41 sseldi ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
69 nn0fz0 ⊢ ( 𝐸 ∈ ℕ0 ↔ 𝐸 ∈ ( 0 ... 𝐸 ) )
70 68 69 sylib ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... 𝐸 ) )
71 18 70 41 20 11 splfv1 ⊢ ( 𝜑 → ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) )
72 66 71 syl5eq ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) )
73 9 57 mpdan ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 )
74 72 73 eqtr3d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 )
75 74 fveq2d ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ◡ 𝑊 ‘ 𝐾 ) )
76 65 75 eqtr3d ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) = ( ◡ 𝑊 ‘ 𝐾 ) )
77 76 oveq1d ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) = ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) )
78 77 fveq2d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) ) = ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
79 49 59 78 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
80 8 a1i ⊢ ( 𝜑 → 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) )
81 80 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
82 68 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
83 simpr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) ) → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) )
84 7 a1i ⊢ ( 𝜑 → 𝐸 = ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) )
85 84 oveq1d ⊢ ( 𝜑 → ( 𝐸 − 1 ) = ( ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) − 1 ) )
86 elfzonn0 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
87 38 86 syl ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
88 87 nn0cnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℂ )
89 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
90 88 89 pncand ⊢ ( 𝜑 → ( ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) − 1 ) = ( ◡ 𝑊 ‘ 𝐽 ) )
91 85 90 eqtr2d ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) = ( 𝐸 − 1 ) )
92 91 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) = ( 𝐸 − 1 ) )
93 simpr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) )
94 76 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( ◡ 𝑈 ‘ 𝐾 ) = ( ◡ 𝑊 ‘ 𝐾 ) )
95 92 93 94 3eqtr2rd ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( ◡ 𝑊 ‘ 𝐾 ) = ( ◡ 𝑊 ‘ 𝐽 ) )
96 95 fveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) = ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) )
97 f1ocnvfv2 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝐾 ∈ ran 𝑊 ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) = 𝐾 )
98 61 9 97 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) = 𝐾 )
99 98 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) = 𝐾 )
100 f1ocnvfv2 ⊢ ( ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ 𝐽 ∈ ran 𝑊 ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
101 61 6 100 syl2anc ⊢ ( 𝜑 → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
102 101 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐽 ) ) = 𝐽 )
103 96 99 102 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → 𝐾 = 𝐽 )
104 10 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → 𝐾 ≠ 𝐽 )
105 103 104 pm2.21ddne ⊢ ( ( 𝜑 ∧ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) )
106 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
107 nn0p1nn ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
108 87 107 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
109 7 108 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
110 0p1e1 ⊢ ( 0 + 1 ) = 1
111 110 fveq2i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ( ℤ≥ ‘ 1 )
112 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
113 111 112 eqtr4i ⊢ ( ℤ≥ ‘ ( 0 + 1 ) ) = ℕ
114 109 113 eleqtrrdi ⊢ ( 𝜑 → 𝐸 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
115 fzosplitsnm1 ⊢ ( ( 0 ∈ ℤ ∧ 𝐸 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( 0 ..^ 𝐸 ) = ( ( 0 ..^ ( 𝐸 − 1 ) ) ∪ { ( 𝐸 − 1 ) } ) )
116 106 114 115 syl2anc ⊢ ( 𝜑 → ( 0 ..^ 𝐸 ) = ( ( 0 ..^ ( 𝐸 − 1 ) ) ∪ { ( 𝐸 − 1 ) } ) )
117 11 116 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( ( 0 ..^ ( 𝐸 − 1 ) ) ∪ { ( 𝐸 − 1 ) } ) )
118 fvex ⊢ ( ◡ 𝑈 ‘ 𝐾 ) ∈ V
119 elunsn ⊢ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ V → ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( ( 0 ..^ ( 𝐸 − 1 ) ) ∪ { ( 𝐸 − 1 ) } ) ↔ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) ) )
120 118 119 ax-mp ⊢ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( ( 0 ..^ ( 𝐸 − 1 ) ) ∪ { ( 𝐸 − 1 ) } ) ↔ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) )
121 117 120 sylib ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) ∨ ( ◡ 𝑈 ‘ 𝐾 ) = ( 𝐸 − 1 ) ) )
122 83 105 121 mpjaodan ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) )
123 elfzom1elp1fzo ⊢ ( ( 𝐸 ∈ ℤ ∧ ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( 𝐸 − 1 ) ) ) → ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) ∈ ( 0 ..^ 𝐸 ) )
124 82 122 123 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) ∈ ( 0 ..^ 𝐸 ) )
125 77 124 eqeltrrd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ∈ ( 0 ..^ 𝐸 ) )
126 18 70 41 20 125 splfv1 ⊢ ( 𝜑 → ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
127 81 126 eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
128 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
129 82 128 zsubcld ⊢ ( 𝜑 → ( 𝐸 − 1 ) ∈ ℤ )
130 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
131 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
132 131 biimpi ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
133 18 130 132 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
134 elfzelz ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℤ )
135 133 134 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
136 135 128 zsubcld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ )
137 109 nnred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
138 135 zred ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
139 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
140 elfzle2 ⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐸 ≤ ( ♯ ‘ 𝑊 ) )
141 41 140 syl ⊢ ( 𝜑 → 𝐸 ≤ ( ♯ ‘ 𝑊 ) )
142 137 138 139 141 lesub1dd ⊢ ( 𝜑 → ( 𝐸 − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) )
143 eluz ⊢ ( ( ( 𝐸 − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 − 1 ) ) ↔ ( 𝐸 − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
144 143 biimpar ⊢ ( ( ( ( 𝐸 − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ℤ ) ∧ ( 𝐸 − 1 ) ≤ ( ( ♯ ‘ 𝑊 ) − 1 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 − 1 ) ) )
145 129 136 142 144 syl21anc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 − 1 ) ) )
146 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 − 1 ) ) → ( 0 ..^ ( 𝐸 − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
147 145 146 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝐸 − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
148 147 122 sseldd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
149 76 148 eqeltrrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐾 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
150 1 3 18 31 149 cycpmfv1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) ) = ( 𝑊 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
151 98 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ◡ 𝑊 ‘ 𝐾 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )
152 127 150 151 3eqtr2rd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) = ( 𝑈 ‘ ( ( ◡ 𝑊 ‘ 𝐾 ) + 1 ) ) )
153 79 152 eqtr4d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )