cshf1o

Description: Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023)

		Ref	Expression
	Assertion	cshf1o	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran W$

Proof

Step	Hyp	Ref	Expression
1		cshwrnid	$⊢ (W \in Word D \land N \in ℤ) \to ran (W cyclShift N) = ran W$
2	1	3adant2	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to ran (W cyclShift N) = ran W$
3		wrddm	$⊢ W \in Word D \to dom W = (0 ..^\|W\|)$
4	3	3ad2ant1	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to dom W = (0 ..^\|W\|)$
5		simp2	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to W : dom W \underset{1-1}{⟶} D$
6		f1eq2	$⊢ dom W = (0 ..^\|W\|) \to (W : dom W \underset{1-1}{⟶} D \leftrightarrow W : (0 ..^\|W\|) \underset{1-1}{⟶} D)$
7	6	biimpa	$⊢ (dom W = (0 ..^\|W\|) \land W : dom W \underset{1-1}{⟶} D) \to W : (0 ..^\|W\|) \underset{1-1}{⟶} D$
8	4 5 7	syl2anc	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to W : (0 ..^\|W\|) \underset{1-1}{⟶} D$
9		simp3	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to N \in ℤ$
10		eqid	$⊢ W cyclShift N = W cyclShift N$
11		cshf1	$⊢ (W : (0 ..^\|W\|) \underset{1-1}{⟶} D \land N \in ℤ \land W cyclShift N = W cyclShift N) \to (W cyclShift N) : (0 ..^\|W\|) \underset{1-1}{⟶} D$
12	10 11	mp3an3	$⊢ (W : (0 ..^\|W\|) \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : (0 ..^\|W\|) \underset{1-1}{⟶} D$
13	8 9 12	syl2anc	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : (0 ..^\|W\|) \underset{1-1}{⟶} D$
14		f1eq2	$⊢ dom W = (0 ..^\|W\|) \to ((W cyclShift N) : dom W \underset{1-1}{⟶} D \leftrightarrow (W cyclShift N) : (0 ..^\|W\|) \underset{1-1}{⟶} D)$
15	14	biimpar	$⊢ (dom W = (0 ..^\|W\|) \land (W cyclShift N) : (0 ..^\|W\|) \underset{1-1}{⟶} D) \to (W cyclShift N) : dom W \underset{1-1}{⟶} D$
16	4 13 15	syl2anc	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : dom W \underset{1-1}{⟶} D$
17		f1f1orn	$⊢ (W cyclShift N) : dom W \underset{1-1}{⟶} D \to (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran (W cyclShift N)$
18	16 17	syl	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran (W cyclShift N)$
19		f1oeq3	$⊢ ran (W cyclShift N) = ran W \to ((W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran (W cyclShift N) \leftrightarrow (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran W)$
20	19	biimpa	$⊢ (ran (W cyclShift N) = ran W \land (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran (W cyclShift N)) \to (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran W$
21	2 18 20	syl2anc	$⊢ (W \in Word D \land W : dom W \underset{1-1}{⟶} D \land N \in ℤ) \to (W cyclShift N) : dom W \underset{1-1 onto}{⟶} ran W$

Metamath Proof Explorer

Theorem cshf1o

Proof