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 \in Word A \land N \in ℤ) \to (W cyclShift N) : (0 ..^\|W\|) ⟶ A$

Proof

Step	Hyp	Ref	Expression
1		cshwcl	$⊢ W \in Word A \to W cyclShift N \in Word A$
2		wrdf	$⊢ W cyclShift N \in Word A \to (W cyclShift N) : (0 ..^\|W cyclShift N\|) ⟶ A$
3	1 2	syl	$⊢ W \in Word A \to (W cyclShift N) : (0 ..^\|W cyclShift N\|) ⟶ A$
4	3	adantr	$⊢ (W \in Word A \land N \in ℤ) \to (W cyclShift N) : (0 ..^\|W cyclShift N\|) ⟶ A$
5		cshwlen	$⊢ (W \in Word A \land N \in ℤ) \to \|W cyclShift N\| = \|W\|$
6	5	oveq2d	$⊢ (W \in Word A \land N \in ℤ) \to (0 ..^\|W cyclShift N\|) = (0 ..^\|W\|)$
7	6	feq2d	$⊢ (W \in Word A \land N \in ℤ) \to ((W cyclShift N) : (0 ..^\|W cyclShift N\|) ⟶ A \leftrightarrow (W cyclShift N) : (0 ..^\|W\|) ⟶ A)$
8	4 7	mpbid	$⊢ (W \in Word A \land N \in ℤ) \to (W cyclShift N) : (0 ..^\|W\|) ⟶ A$