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 ◡ 𝐺 ) )