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	$⊢ (F \in Word A \land Fun F^{-1} \land S \in ℤ) \to (G = F cyclShift S \to Fun G^{-1})$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ F \in Word A \to F : (0 ..^\|F\|) ⟶ A$
2		df-f1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} A \leftrightarrow (F : (0 ..^\|F\|) ⟶ A \land Fun F^{-1})$
3	2	biimpri	$⊢ (F : (0 ..^\|F\|) ⟶ A \land Fun F^{-1}) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} A$
4	1 3	sylan	$⊢ (F \in Word A \land Fun F^{-1}) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} A$
5	4	3adant3	$⊢ (F \in Word A \land Fun F^{-1} \land S \in ℤ) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} A$
6	5	adantr	$⊢ ((F \in Word A \land Fun F^{-1} \land S \in ℤ) \land G = F cyclShift S) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} A$
7		simpl3	$⊢ ((F \in Word A \land Fun F^{-1} \land S \in ℤ) \land G = F cyclShift S) \to S \in ℤ$
8		simpr	$⊢ ((F \in Word A \land Fun F^{-1} \land S \in ℤ) \land G = F cyclShift S) \to G = F cyclShift S$
9		cshf1	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} A \land S \in ℤ \land G = F cyclShift S) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} A$
10	6 7 8 9	syl3anc	$⊢ ((F \in Word A \land Fun F^{-1} \land S \in ℤ) \land G = F cyclShift S) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} A$
11	10	ex	$⊢ (F \in Word A \land Fun F^{-1} \land S \in ℤ) \to (G = F cyclShift S \to G : (0 ..^\|F\|) \underset{1-1}{⟶} A)$
12		df-f1	$⊢ G : (0 ..^\|F\|) \underset{1-1}{⟶} A \leftrightarrow (G : (0 ..^\|F\|) ⟶ A \land Fun G^{-1})$
13	12	simprbi	$⊢ G : (0 ..^\|F\|) \underset{1-1}{⟶} A \to Fun G^{-1}$
14	11 13	syl6	$⊢ (F \in Word A \land Fun F^{-1} \land S \in ℤ) \to (G = F cyclShift S \to Fun G^{-1})$

Metamath Proof Explorer