Metamath Proof Explorer

Theorem cycpmco2lem2

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 cycpmco2lem2 ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 )

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 ovexd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ V )
10 7 9 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ V )
11 5 eldifad ⊢ ( 𝜑 → 𝐼 ∈ 𝐷 )
12 11 s1cld ⊢ ( 𝜑 → ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 )
13 splval ⊢ ( ( 𝑊 ∈ dom 𝑀 ∧ ( 𝐸 ∈ V ∧ 𝐸 ∈ V ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) ) → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
14 4 10 10 12 13 syl13anc ⊢ ( 𝜑 → ( 𝑊 splice ⟨ 𝐸 , 𝐸 , ⟨“ 𝐼 ”⟩ ⟩ ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
15 8 14 syl5eq ⊢ ( 𝜑 → 𝑈 = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
16 15 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 𝐸 ) )
17 ssrab2 ⊢ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⊆ Word 𝐷
18 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
19 1 2 18 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
20 3 19 syl ⊢ ( 𝜑 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ 𝑆 ) )
21 20 fdmd ⊢ ( 𝜑 → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
22 4 21 eleqtrd ⊢ ( 𝜑 → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
23 17 22 sselid ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
24 pfxcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
25 23 24 syl ⊢ ( 𝜑 → ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 )
26 ccatcl ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ) → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
27 25 12 26 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 )
28 swrdcl ⊢ ( 𝑊 ∈ Word 𝐷 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
29 23 28 syl ⊢ ( 𝜑 → ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 )
30 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝑊 ) ) ⊆ ℕ0
31 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
32 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
33 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
34 31 32 33 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
35 34 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
36 22 35 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
37 36 simprd ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
38 f1cnv ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
39 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
40 37 38 39 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
41 40 6 ffvelrnd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ dom 𝑊 )
42 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
43 23 42 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
44 41 43 eleqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
45 fzofzp1 ⊢ ( ( ◡ 𝑊 ‘ 𝐽 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
46 44 45 syl ⊢ ( 𝜑 → ( ( ◡ 𝑊 ‘ 𝐽 ) + 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
47 7 46 eqeltrid ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
48 30 47 sselid ⊢ ( 𝜑 → 𝐸 ∈ ℕ0 )
49 fzonn0p1 ⊢ ( 𝐸 ∈ ℕ0 → 𝐸 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
50 48 49 syl ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ..^ ( 𝐸 + 1 ) ) )
51 ccatws1len ⊢ ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
52 23 24 51 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) )
53 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
54 23 47 53 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) = 𝐸 )
55 54 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + 1 ) = ( 𝐸 + 1 ) )
56 52 55 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
57 56 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) = ( 0 ..^ ( 𝐸 + 1 ) ) )
58 50 57 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) )
59 ccatval1 ⊢ ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ∈ Word 𝐷 ∧ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝐷 ∧ 𝐸 ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ) ) ) → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 𝐸 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 𝐸 ) )
60 27 29 58 59 syl3anc ⊢ ( 𝜑 → ( ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ++ ( 𝑊 substr ⟨ 𝐸 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ‘ 𝐸 ) = ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 𝐸 ) )
61 48 nn0zd ⊢ ( 𝜑 → 𝐸 ∈ ℤ )
62 elfzomin ⊢ ( 𝐸 ∈ ℤ → 𝐸 ∈ ( 𝐸 ..^ ( 𝐸 + 1 ) ) )
63 61 62 syl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐸 ..^ ( 𝐸 + 1 ) ) )
64 s1len ⊢ ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) = 1
65 64 a1i ⊢ ( 𝜑 → ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) = 1 )
66 54 65 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) = ( 𝐸 + 1 ) )
67 54 66 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) ) = ( 𝐸 ..^ ( 𝐸 + 1 ) ) )
68 63 67 eleqtrrd ⊢ ( 𝜑 → 𝐸 ∈ ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) ) )
69 ccatval2 ⊢ ( ( ( 𝑊 prefix 𝐸 ) ∈ Word 𝐷 ∧ ⟨“ 𝐼 ”⟩ ∈ Word 𝐷 ∧ 𝐸 ∈ ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ..^ ( ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) + ( ♯ ‘ ⟨“ 𝐼 ”⟩ ) ) ) ) → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 𝐸 ) = ( ⟨“ 𝐼 ”⟩ ‘ ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) )
70 25 12 68 69 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑊 prefix 𝐸 ) ++ ⟨“ 𝐼 ”⟩ ) ‘ 𝐸 ) = ( ⟨“ 𝐼 ”⟩ ‘ ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) )
71 16 60 70 3eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = ( ⟨“ 𝐼 ”⟩ ‘ ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) )
72 54 oveq2d ⊢ ( 𝜑 → ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = ( 𝐸 − 𝐸 ) )
73 48 nn0cnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
74 73 subidd ⊢ ( 𝜑 → ( 𝐸 − 𝐸 ) = 0 )
75 72 74 eqtrd ⊢ ( 𝜑 → ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) = 0 )
76 75 fveq2d ⊢ ( 𝜑 → ( ⟨“ 𝐼 ”⟩ ‘ ( 𝐸 − ( ♯ ‘ ( 𝑊 prefix 𝐸 ) ) ) ) = ( ⟨“ 𝐼 ”⟩ ‘ 0 ) )
77 s1fv ⊢ ( 𝐼 ∈ ( 𝐷 ∖ ran 𝑊 ) → ( ⟨“ 𝐼 ”⟩ ‘ 0 ) = 𝐼 )
78 5 77 syl ⊢ ( 𝜑 → ( ⟨“ 𝐼 ”⟩ ‘ 0 ) = 𝐼 )
79 71 76 78 3eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐸 ) = 𝐼 )