Metamath Proof Explorer

Theorem cycpmconjslem1

Description: Lemma for cycpmconjs . (Contributed by Thierry Arnoux, 14-Oct-2023)

Ref Expression
Hypotheses cycpmconjs.c ⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) )
cycpmconjs.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmconjs.n ⊢ 𝑁 = ( ♯ ‘ 𝐷 )
cycpmconjs.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmconjslem1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
cycpmconjslem1.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
cycpmconjslem1.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmconjslem1.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑃 )
Assertion cycpmconjslem1 ( 𝜑 → ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )

Proof

Step Hyp Ref Expression
1 cycpmconjs.c ⊢ 𝐶 = ( 𝑀 “ ( ◡ ♯ “ { 𝑃 } ) )
2 cycpmconjs.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3 cycpmconjs.n ⊢ 𝑁 = ( ♯ ‘ 𝐷 )
4 cycpmconjs.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
5 cycpmconjslem1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
6 cycpmconjslem1.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
7 cycpmconjslem1.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
8 cycpmconjslem1.2 ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) = 𝑃 )
9 resco ⊢ ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ↾ ran 𝑊 ) = ( ◡ 𝑊 ∘ ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) )
10 9 coeq1i ⊢ ( ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ↾ ran 𝑊 ) ∘ 𝑊 ) = ( ( ◡ 𝑊 ∘ ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ) ∘ 𝑊 )
11 ssid ⊢ ran 𝑊 ⊆ ran 𝑊
12 cores ⊢ ( ran 𝑊 ⊆ ran 𝑊 → ( ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ↾ ran 𝑊 ) ∘ 𝑊 ) = ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 ) )
13 11 12 ax-mp ⊢ ( ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ↾ ran 𝑊 ) ∘ 𝑊 ) = ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 )
14 coass ⊢ ( ( ◡ 𝑊 ∘ ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ) ∘ 𝑊 ) = ( ◡ 𝑊 ∘ ( ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ∘ 𝑊 ) )
15 10 13 14 3eqtr3i ⊢ ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 ) = ( ◡ 𝑊 ∘ ( ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ∘ 𝑊 ) )
16 4 5 6 7 tocycfvres1 ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) = ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) )
17 16 coeq1d ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ∘ 𝑊 ) = ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ 𝑊 ) )
18 coass ⊢ ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ 𝑊 ) = ( ( 𝑊 cyclShift 1 ) ∘ ( ◡ 𝑊 ∘ 𝑊 ) )
19 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
20 f1ococnv1 ⊢ ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 → ( ◡ 𝑊 ∘ 𝑊 ) = ( I ↾ dom 𝑊 ) )
21 7 19 20 3syl ⊢ ( 𝜑 → ( ◡ 𝑊 ∘ 𝑊 ) = ( I ↾ dom 𝑊 ) )
22 21 coeq2d ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ∘ ( ◡ 𝑊 ∘ 𝑊 ) ) = ( ( 𝑊 cyclShift 1 ) ∘ ( I ↾ dom 𝑊 ) ) )
23 coires1 ⊢ ( ( 𝑊 cyclShift 1 ) ∘ ( I ↾ dom 𝑊 ) ) = ( ( 𝑊 cyclShift 1 ) ↾ dom 𝑊 )
24 22 23 eqtr2di ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ↾ dom 𝑊 ) = ( ( 𝑊 cyclShift 1 ) ∘ ( ◡ 𝑊 ∘ 𝑊 ) ) )
25 18 24 eqtr4id ⊢ ( 𝜑 → ( ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ 𝑊 ) = ( ( 𝑊 cyclShift 1 ) ↾ dom 𝑊 ) )
26 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
27 cshwfn ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ) → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
28 6 26 27 syl2anc ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
29 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
30 6 29 syl ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
31 30 fneq2d ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) Fn dom 𝑊 ↔ ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) )
32 28 31 mpbird ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) Fn dom 𝑊 )
33 fnresdm ⊢ ( ( 𝑊 cyclShift 1 ) Fn dom 𝑊 → ( ( 𝑊 cyclShift 1 ) ↾ dom 𝑊 ) = ( 𝑊 cyclShift 1 ) )
34 32 33 syl ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ↾ dom 𝑊 ) = ( 𝑊 cyclShift 1 ) )
35 17 25 34 3eqtrd ⊢ ( 𝜑 → ( ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ∘ 𝑊 ) = ( 𝑊 cyclShift 1 ) )
36 35 coeq2d ⊢ ( 𝜑 → ( ◡ 𝑊 ∘ ( ( ( 𝑀 ‘ 𝑊 ) ↾ ran 𝑊 ) ∘ 𝑊 ) ) = ( ◡ 𝑊 ∘ ( 𝑊 cyclShift 1 ) ) )
37 15 36 syl5eq ⊢ ( 𝜑 → ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 ) = ( ◡ 𝑊 ∘ ( 𝑊 cyclShift 1 ) ) )
38 wrdfn ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
39 6 38 syl ⊢ ( 𝜑 → 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
40 df-f ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ran 𝑊 ↔ ( 𝑊 Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ran 𝑊 ⊆ ran 𝑊 ) )
41 39 11 40 sylanblrc ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ran 𝑊 )
42 iswrdi ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ ran 𝑊 → 𝑊 ∈ Word ran 𝑊 )
43 41 42 syl ⊢ ( 𝜑 → 𝑊 ∈ Word ran 𝑊 )
44 f1ocnv ⊢ ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
45 7 19 44 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
46 f1of ⊢ ( ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
47 45 46 syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 )
48 cshco ⊢ ( ( 𝑊 ∈ Word ran 𝑊 ∧ 1 ∈ ℤ ∧ ◡ 𝑊 : ran 𝑊 ⟶ dom 𝑊 ) → ( ◡ 𝑊 ∘ ( 𝑊 cyclShift 1 ) ) = ( ( ◡ 𝑊 ∘ 𝑊 ) cyclShift 1 ) )
49 43 26 47 48 syl3anc ⊢ ( 𝜑 → ( ◡ 𝑊 ∘ ( 𝑊 cyclShift 1 ) ) = ( ( ◡ 𝑊 ∘ 𝑊 ) cyclShift 1 ) )
50 8 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑊 ) ) = ( 0 ..^ 𝑃 ) )
51 30 50 eqtrd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ 𝑃 ) )
52 51 reseq2d ⊢ ( 𝜑 → ( I ↾ dom 𝑊 ) = ( I ↾ ( 0 ..^ 𝑃 ) ) )
53 21 52 eqtrd ⊢ ( 𝜑 → ( ◡ 𝑊 ∘ 𝑊 ) = ( I ↾ ( 0 ..^ 𝑃 ) ) )
54 53 oveq1d ⊢ ( 𝜑 → ( ( ◡ 𝑊 ∘ 𝑊 ) cyclShift 1 ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )
55 37 49 54 3eqtrd ⊢ ( 𝜑 → ( ( ◡ 𝑊 ∘ ( 𝑀 ‘ 𝑊 ) ) ∘ 𝑊 ) = ( ( I ↾ ( 0 ..^ 𝑃 ) ) cyclShift 1 ) )