Metamath Proof Explorer

Theorem cycpmco2lem3

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 cycpmco2lem3 ( 𝜑 → ( ( ♯ ‘ 𝑈 ) − 1 ) = ( ♯ ‘ 𝑊 ) )

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