Metamath Proof Explorer

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 ⊢ W ∈ Word A ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W ⟶ A

Proof

Step Hyp Ref Expression
1 cshwcl ⊢ W ∈ Word A → W cyclShift N ∈ Word A
2 wrdf ⊢ W cyclShift N ∈ Word A → W cyclShift N : 0 ..^ W cyclShift N ⟶ A
3 1 2 syl ⊢ W ∈ Word A → W cyclShift N : 0 ..^ W cyclShift N ⟶ A
4 3 adantr ⊢ W ∈ Word A ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W cyclShift N ⟶ A
5 cshwlen ⊢ W ∈ Word A ∧ N ∈ ℤ → W cyclShift N = W
6 5 oveq2d ⊢ W ∈ Word A ∧ N ∈ ℤ → 0 ..^ W cyclShift N = 0 ..^ W
7 6 feq2d ⊢ W ∈ Word A ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W cyclShift N ⟶ A ↔ W cyclShift N : 0 ..^ W ⟶ A
8 4 7 mpbid ⊢ W ∈ Word A ∧ N ∈ ℤ → W cyclShift N : 0 ..^ W ⟶ A