This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cshinj

Description: If a word is injectiv (regarded as function), the cyclically shifted word is also injective. (Contributed by AV, 14-Mar-2021)

Ref Expression
Assertion cshinj ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → Fun ◡ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 wrdf ⊢ ( 𝐹 ∈ Word 𝐴 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
2 df-f1 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ Fun ◡ 𝐹 ) )
3 2 biimpri ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ Fun ◡ 𝐹 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
4 1 3 sylan ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
5 4 3adant3 ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
6 5 adantr ⊢ ( ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
7 simpl3 ⊢ ( ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝑆 ∈ ℤ )
8 simpr ⊢ ( ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 = ( 𝐹 cyclShift 𝑆 ) )
9 cshf1 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )
11 10 ex ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ) )
12 df-f1 ⊢ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ↔ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ Fun ◡ 𝐺 ) )
13 12 simprbi ⊢ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → Fun ◡ 𝐺 )
14 11 13 syl6 ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ Fun ◡ 𝐹 ∧ 𝑆 ∈ ℤ ) → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → Fun ◡ 𝐺 ) )