Metamath Proof Explorer

Theorem cshf1o

Description: Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023)

Ref Expression
Assertion cshf1o ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran 𝑊 )

Proof

Step Hyp Ref Expression
1 cshwrnid ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 )
2 1 3adant2 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 )
3 wrddm ⊢ ( 𝑊 ∈ Word 𝐷 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
4 3 3ad2ant1 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
5 simp2 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
6 f1eq2 ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 : dom 𝑊 –1-1→ 𝐷 ↔ 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 ) )
7 6 biimpa ⊢ ( ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 )
8 4 5 7 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 )
9 simp3 ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
10 eqid ⊢ ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift 𝑁 )
11 cshf1 ⊢ ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ∧ ( 𝑊 cyclShift 𝑁 ) = ( 𝑊 cyclShift 𝑁 ) ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 )
12 10 11 mp3an3 ⊢ ( ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 )
13 8 9 12 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 )
14 f1eq2 ⊢ ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1→ 𝐷 ↔ ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 ) )
15 14 biimpar ⊢ ( ( dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ∧ ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) –1-1→ 𝐷 ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1→ 𝐷 )
16 4 13 15 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1→ 𝐷 )
17 f1f1orn ⊢ ( ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1→ 𝐷 → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran ( 𝑊 cyclShift 𝑁 ) )
18 16 17 syl ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran ( 𝑊 cyclShift 𝑁 ) )
19 f1oeq3 ⊢ ( ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 → ( ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran ( 𝑊 cyclShift 𝑁 ) ↔ ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran 𝑊 ) )
20 19 biimpa ⊢ ( ( ran ( 𝑊 cyclShift 𝑁 ) = ran 𝑊 ∧ ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran ( 𝑊 cyclShift 𝑁 ) ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran 𝑊 )
21 2 18 20 syl2anc ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : dom 𝑊 –1-1-onto→ ran 𝑊 )