Metamath Proof Explorer

Theorem cycpmco2lem6

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 𝑊 )
cycpmco2lem6.2 ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
cycpmco2lem6.1 ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
Assertion cycpmco2lem6 ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )

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 cycpmco2lem6.2 ⊢ ( 𝜑 → 𝐾 ≠ 𝐼 )
11 cycpmco2lem6.1 ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
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 sselid ⊢ ( 𝜑 → 𝑊 ∈ 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 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
26 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
27 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
28 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
29 26 27 28 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
30 29 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
31 17 30 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
32 31 simprd ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
33 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
34 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
35 32 33 34 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
36 35 6 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
37 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
38 18 37 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 36 38 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
41 39 40 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
42 7 41 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
43 25 42 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
44 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
45 43 44 eleqtrdi ⊢ ( 𝜑 → 𝐸 ∈ ( ℤ≥ ‘ 0 ) )
46 fzoss1 ⊢ ( 𝐸 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) )
47 45 46 syl ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ⊆ ( 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 9 57 mpdan ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = 𝐾 )
59 58 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ) = ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) )
60 8 a1i ⊢ ( 𝜑 → 𝑈 = ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) )
61 fzossz ⊢ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ⊆ ℤ
62 61 11 sselid ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ℤ )
63 62 zcnd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ℂ )
64 43 nn0cnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
65 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
66 63 64 65 nppcan3d ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) = ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) )
67 66 eqcomd ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) = ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) )
68 60 67 fveq12d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) + 1 ) ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) )
69 49 59 68 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) )
70 63 64 npcand ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + 𝐸 ) = ( ◡ 𝑈 ‘ 𝐾 ) )
71 70 fveq2d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) )
72 nn0fz0 ⊢ ( 𝐸 ∈ ℕ0 ↔ 𝐸 ∈ ( 0 ... 𝐸 ) )
73 43 72 sylib ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... 𝐸 ) )
74 lencl ⊢ ( 𝑊 ∈ Word 𝐷 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
75 18 74 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
76 75 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
77 ovexd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V )
78 7 77 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ V )
79 splval ⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
80 4 78 78 20 79 syl13anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
81 8 80 eqtrid ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
82 81 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
83 pfxcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
84 18 83 syl ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
85 ccatcl ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
86 84 20 85 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
87 swrdcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
88 18 87 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
89 ccatlen ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ) → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
90 86 88 89 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
91 ccatws1len ⊢ ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
92 18 83 91 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
93 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
94 18 42 93 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) )
96 92 95 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
97 nn0fz0 ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
98 75 97 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
99 swrdlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
100 18 42 98 99 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝐸 ) )
101 96 100 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
102 82 90 101 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
103 43 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
104 103 peano2zd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℤ )
105 104 zcnd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ∈ ℂ )
106 105 76 64 addsubassd ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + 1 ) + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
107 64 65 76 addassd ⊢ ( 𝜑 → ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) = ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) )
108 107 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐸 + 1 ) + ( ♯ ‘ 𝑊 ) ) − 𝐸 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
109 102 106 108 3eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) )
110 65 76 addcld ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
111 64 110 pncan2d ⊢ ( 𝜑 → ( ( 𝐸 + ( 1 + ( ♯ ‘ 𝑊 ) ) ) − 𝐸 ) = ( 1 + ( ♯ ‘ 𝑊 ) ) )
112 65 76 addcomd ⊢ ( 𝜑 → ( 1 + ( ♯ ‘ 𝑊 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
113 109 111 112 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
114 76 65 113 mvrraddd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )
115 114 oveq2d ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) = ( 𝐸 ..^ ( ♯ ‘ 𝑊 ) ) )
116 11 115 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 𝐸 ..^ ( ♯ ‘ 𝑊 ) ) )
117 fzosubel ⊢ ( ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 𝐸 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝐸 ∈ ℤ ) → ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) ∈ ( ( 𝐸 − 𝐸 ) ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
118 116 103 117 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) ∈ ( ( 𝐸 − 𝐸 ) ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
119 64 subidd ⊢ ( 𝜑 → ( 𝐸 − 𝐸 ) = 0 )
120 119 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 − 𝐸 ) ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
121 118 120 eleqtrd ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
122 65 64 addcomd ⊢ ( 𝜑 → ( 1 + 𝐸 ) = ( 𝐸 + 1 ) )
123 s1len ⊢ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) = 1
124 123 oveq2i ⊢ ( 𝐸 + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 )
125 122 124 eqtr4di ⊢ ( 𝜑 → ( 1 + 𝐸 ) = ( 𝐸 + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) )
126 18 73 42 20 121 125 splfv3 ⊢ ( 𝜑 → ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) = ( 𝑊 ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + 𝐸 ) ) )
127 114 oveq1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
128 127 oveq2d ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) = ( 𝐸 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
129 fzoss1 ⊢ ( 𝐸 ∈ ( ℤ≥ ‘ 0 ) → ( 𝐸 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
130 45 129 syl ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
131 128 130 eqsstrd ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
132 f1ocnvdm ⊢ ( ( 𝑈 : dom 𝑈 –1-1-onto→ ran 𝑈 ∧ 𝐾 ∈ ran 𝑈 ) → ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 )
133 51 55 132 syl2an2r ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ran 𝑊 ) → ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 )
134 9 133 mpdan ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 )
135 75 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
136 135 peano2zd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℤ )
137 elfzonn0 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 )
138 nn0p1nn ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ℕ0 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
139 39 137 138 3syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ℕ )
140 7 139 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ℕ )
141 140 nnred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
142 135 zred ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
143 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
144 elfzle2 ⊢ ( 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝐸 ≤ ( ♯ ‘ 𝑊 ) )
145 42 144 syl ⊢ ( 𝜑 → 𝐸 ≤ ( ♯ ‘ 𝑊 ) )
146 141 142 143 145 leadd1dd ⊢ ( 𝜑 → ( 𝐸 + 1 ) ≤ ( ( ♯ ‘ 𝑊 ) + 1 ) )
147 eluz2 ⊢ ( ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 + 1 ) ) ↔ ( ( 𝐸 + 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ℤ ∧ ( 𝐸 + 1 ) ≤ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
148 104 136 146 147 syl3anbrc ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 + 1 ) ) )
149 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑊 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝐸 + 1 ) ) → ( 0 ..^ ( 𝐸 + 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
150 148 149 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝐸 + 1 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
151 fzonn0p1 ⊢ ( 𝐸 ∈ ℕ0 → 𝐸 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
152 43 151 syl ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
153 150 152 sseldd ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
154 113 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑈 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
155 153 154 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
156 wrddm ⊢ ( 𝑈 ∈ Word 𝐷 → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
157 23 156 syl ⊢ ( 𝜑 → dom 𝑈 = ( 0 ..^ ( ♯ ‘ 𝑈 ) ) )
158 155 157 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ dom 𝑈 )
159 1 2 3 4 5 6 7 8 cycpmco2lem2 ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 )
160 10 58 159 3netr4d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ≠ ( 𝑈 ‘ 𝐸 ) )
161 f1fveq ⊢ ( ( 𝑈 : dom 𝑈 –1-1→ 𝐷 ∧ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈 ) ) → ( ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( 𝑈 ‘ 𝐸 ) ↔ ( ◡ 𝑈 ‘ 𝐾 ) = 𝐸 ) )
162 161 necon3bid ⊢ ( ( 𝑈 : dom 𝑈 –1-1→ 𝐷 ∧ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈 ) ) → ( ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ≠ ( 𝑈 ‘ 𝐸 ) ↔ ( ◡ 𝑈 ‘ 𝐾 ) ≠ 𝐸 ) )
163 162 biimp3a ⊢ ( ( 𝑈 : dom 𝑈 –1-1→ 𝐷 ∧ ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ dom 𝑈 ∧ 𝐸 ∈ dom 𝑈 ) ∧ ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) ≠ ( 𝑈 ‘ 𝐸 ) ) → ( ◡ 𝑈 ‘ 𝐾 ) ≠ 𝐸 )
164 24 134 158 160 163 syl121anc ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) ≠ 𝐸 )
165 fzom1ne1 ⊢ ( ( ( ◡ 𝑈 ‘ 𝐾 ) ∈ ( 𝐸 ..^ ( ( ♯ ‘ 𝑈 ) − 1 ) ) ∧ ( ◡ 𝑈 ‘ 𝐾 ) ≠ 𝐸 ) → ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) )
166 11 164 165 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) )
167 131 166 sseldd ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) )
168 1 3 18 32 167 cycpmfv1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ) ) = ( 𝑊 ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) + 1 ) ) )
169 63 65 64 subsub4d ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) = ( ( ◡ 𝑈 ‘ 𝐾 ) − ( 1 + 𝐸 ) ) )
170 169 oveq1d ⊢ ( 𝜑 → ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) = ( ( ( ◡ 𝑈 ‘ 𝐾 ) − ( 1 + 𝐸 ) ) + ( 1 + 𝐸 ) ) )
171 65 64 addcld ⊢ ( 𝜑 → ( 1 + 𝐸 ) ∈ ℂ )
172 63 171 npcand ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − ( 1 + 𝐸 ) ) + ( 1 + 𝐸 ) ) = ( ◡ 𝑈 ‘ 𝐾 ) )
173 170 172 eqtr2d ⊢ ( 𝜑 → ( ◡ 𝑈 ‘ 𝐾 ) = ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) )
174 60 173 fveq12d ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) )
175 64 76 pncan3d ⊢ ( 𝜑 → ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) = ( ♯ ‘ 𝑊 ) )
176 114 135 eqeltrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) ∈ ℤ )
177 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
178 176 177 zsubcld ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ∈ ℤ )
179 178 zred ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ∈ ℝ )
180 114 142 eqeltrd ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) ∈ ℝ )
181 180 ltm1d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) < ( ( ♯ ‘ 𝑈 ) − 1 ) )
182 181 114 breqtrd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) < ( ♯ ‘ 𝑊 ) )
183 179 142 182 ltled ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) )
184 eluz1 ⊢ ( ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ∈ ℤ → ( ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) ↔ ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
185 184 biimpar ⊢ ( ( ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ∈ ℤ ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℤ ∧ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ≤ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) )
186 178 135 183 185 syl12anc ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) )
187 175 186 eqeltrd ⊢ ( 𝜑 → ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) )
188 fzoss2 ⊢ ( ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ∈ ( ℤ≥ ‘ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) → ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) ⊆ ( 𝐸 ..^ ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) )
189 187 188 syl ⊢ ( 𝜑 → ( 𝐸 ..^ ( ( ( ♯ ‘ 𝑈 ) − 1 ) − 1 ) ) ⊆ ( 𝐸 ..^ ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) )
190 189 166 sseldd ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ( 𝐸 ..^ ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) )
191 135 103 zsubcld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℤ )
192 fzosubel3 ⊢ ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ( 𝐸 ..^ ( 𝐸 + ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) ) ∧ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ∈ ℤ ) → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
193 190 191 192 syl2anc ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 𝐸 ) ) )
194 18 73 42 20 193 125 splfv3 ⊢ ( 𝜑 → ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) = ( 𝑊 ‘ ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + 𝐸 ) ) )
195 63 65 subcld ⊢ ( 𝜑 → ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ∈ ℂ )
196 195 64 npcand ⊢ ( 𝜑 → ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + 𝐸 ) = ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) )
197 196 fveq2d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) − 𝐸 ) + 𝐸 ) ) = ( 𝑊 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ) )
198 174 194 197 3eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) = ( 𝑊 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ) )
199 198 58 eqtr3d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ) = 𝐾 )
200 199 fveq2d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ ( 𝑊 ‘ ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) ) ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )
201 63 65 npcand ⊢ ( 𝜑 → ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) + 1 ) = ( ◡ 𝑈 ‘ 𝐾 ) )
202 201 fveq2d ⊢ ( 𝜑 → ( 𝑊 ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 1 ) + 1 ) ) = ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) )
203 168 200 202 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) = ( 𝑊 ‘ ( ◡ 𝑈 ‘ 𝐾 ) ) )
204 71 126 203 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) = ( ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) ‘ ( ( ( ◡ 𝑈 ‘ 𝐾 ) − 𝐸 ) + ( 1 + 𝐸 ) ) ) )
205 69 204 eqtr4d ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑈 ) ‘ 𝐾 ) = ( ( 𝑀 ‘ 𝑊 ) ‘ 𝐾 ) )