Theorem cshwf

Description: A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018)

	Ref	Expression
Assertion	cshwf	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cshwcl	⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝐴 )
2		wrdf	⊢ ( ( 𝑊 cyclShift 𝑁 ) ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
3	1 2	syl	⊢ ( 𝑊 ∈ Word 𝐴 → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
4	3	adantr	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 )
5		cshwlen	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) = ( ♯ ‘ 𝑊 ) )
6	5	oveq2d	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
7	6	feq2d	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ ( 𝑊 cyclShift 𝑁 ) ) ) ⟶ 𝐴 ↔ ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 ) )
8	4 7	mpbid	⊢ ( ( 𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ) → ( 𝑊 cyclShift 𝑁 ) : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐴 )