Metamath Proof Explorer

Theorem cycpmcl

Description: Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
cycpmcl.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
Assertion cycpmcl ( 𝜑 → ( 𝐶 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 tocycval.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycfv.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3 tocycfv.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝐷 )
4 tocycfv.1 ⊢ ( 𝜑 → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
5 cycpmcl.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
6 f1oi ⊢ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) : ( 𝐷 ∖ ran 𝑊 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑊 )
7 6 a1i ⊢ ( 𝜑 → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) : ( 𝐷 ∖ ran 𝑊 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑊 ) )
8 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
9 cshwf ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ) → ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
10 3 8 9 syl2anc ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
11 10 ffnd ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
12 df-f1 ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
13 4 12 sylib ⊢ ( 𝜑 → ( 𝑊 : dom 𝑊 ⟶ 𝐷 ∧ Fun ◡ 𝑊 ) )
14 13 simprd ⊢ ( 𝜑 → Fun ◡ 𝑊 )
15 eqid ⊢ ( 𝑊 cyclShift 1 ) = ( 𝑊 cyclShift 1 )
16 cshinj ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ Fun ◡ 𝑊 ∧ 1 ∈ ℤ ) → ( ( 𝑊 cyclShift 1 ) = ( 𝑊 cyclShift 1 ) → Fun ◡ ( 𝑊 cyclShift 1 ) ) )
17 15 16 mpi ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ Fun ◡ 𝑊 ∧ 1 ∈ ℤ ) → Fun ◡ ( 𝑊 cyclShift 1 ) )
18 3 14 8 17 syl3anc ⊢ ( 𝜑 → Fun ◡ ( 𝑊 cyclShift 1 ) )
19 f1orn ⊢ ( ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ran ( 𝑊 cyclShift 1 ) ↔ ( ( 𝑊 cyclShift 1 ) Fn ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ Fun ◡ ( 𝑊 cyclShift 1 ) ) )
20 11 18 19 sylanbrc ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ran ( 𝑊 cyclShift 1 ) )
21 eqidd ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) = ( 𝑊 cyclShift 1 ) )
22 wrdf ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
23 3 22 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
24 23 fdmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
25 cshwrnid ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ) → ran ( 𝑊 cyclShift 1 ) = ran 𝑊 )
26 3 8 25 syl2anc ⊢ ( 𝜑 → ran ( 𝑊 cyclShift 1 ) = ran 𝑊 )
27 26 eqcomd ⊢ ( 𝜑 → ran 𝑊 = ran ( 𝑊 cyclShift 1 ) )
28 21 24 27 f1oeq123d ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) : dom 𝑊 –1-1-onto→ ran 𝑊 ↔ ( 𝑊 cyclShift 1 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1-onto→ ran ( 𝑊 cyclShift 1 ) ) )
29 20 28 mpbird ⊢ ( 𝜑 → ( 𝑊 cyclShift 1 ) : dom 𝑊 –1-1-onto→ ran 𝑊 )
30 f1f1orn ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 )
31 f1ocnv ⊢ ( 𝑊 : dom 𝑊 –1-1-onto→ ran 𝑊 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
32 4 30 31 3syl ⊢ ( 𝜑 → ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 )
33 f1oco ⊢ ( ( ( 𝑊 cyclShift 1 ) : dom 𝑊 –1-1-onto→ ran 𝑊 ∧ ◡ 𝑊 : ran 𝑊 –1-1-onto→ dom 𝑊 ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) : ran 𝑊 –1-1-onto→ ran 𝑊 )
34 29 32 33 syl2anc ⊢ ( 𝜑 → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) : ran 𝑊 –1-1-onto→ ran 𝑊 )
35 disjdifr ⊢ ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅
36 35 a1i ⊢ ( 𝜑 → ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ )
37 f1oun ⊢ ( ( ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) : ( 𝐷 ∖ ran 𝑊 ) –1-1-onto→ ( 𝐷 ∖ ran 𝑊 ) ∧ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) : ran 𝑊 –1-1-onto→ ran 𝑊 ) ∧ ( ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ ∧ ( ( 𝐷 ∖ ran 𝑊 ) ∩ ran 𝑊 ) = ∅ ) ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) : ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) –1-1-onto→ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) )
38 7 34 36 36 37 syl22anc ⊢ ( 𝜑 → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) : ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) –1-1-onto→ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) )
39 1 2 3 4 tocycfv ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
40 23 frnd ⊢ ( 𝜑 → ran 𝑊 ⊆ 𝐷 )
41 undif ⊢ ( ran 𝑊 ⊆ 𝐷 ↔ ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) = 𝐷 )
42 40 41 sylib ⊢ ( 𝜑 → ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) = 𝐷 )
43 uncom ⊢ ( ran 𝑊 ∪ ( 𝐷 ∖ ran 𝑊 ) ) = ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 )
44 42 43 eqtr3di ⊢ ( 𝜑 → 𝐷 = ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) )
45 39 44 44 f1oeq123d ⊢ ( 𝜑 → ( ( 𝐶 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 ↔ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) : ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) –1-1-onto→ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) ) )
46 38 45 mpbird ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 )
47 fvex ⊢ ( 𝐶 ‘ 𝑊 ) ∈ V
48 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
49 5 48 elsymgbas2 ⊢ ( ( 𝐶 ‘ 𝑊 ) ∈ V → ( ( 𝐶 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) ↔ ( 𝐶 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 ) )
50 47 49 ax-mp ⊢ ( ( 𝐶 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) ↔ ( 𝐶 ‘ 𝑊 ) : 𝐷 –1-1-onto→ 𝐷 )
51 46 50 sylibr ⊢ ( 𝜑 → ( 𝐶 ‘ 𝑊 ) ∈ ( Base ‘ 𝑆 ) )