Metamath Proof Explorer

Theorem 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 ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ → G = F cyclShift S → Fun ⁡ G -1

Proof

Step Hyp Ref Expression
1 wrdf ⊢ F ∈ Word A → F : 0 ..^ F ⟶ A
2 df-f1 ⊢ F : 0 ..^ F ⟶ 1-1 A ↔ F : 0 ..^ F ⟶ A ∧ Fun ⁡ F -1
3 2 biimpri ⊢ F : 0 ..^ F ⟶ A ∧ Fun ⁡ F -1 → F : 0 ..^ F ⟶ 1-1 A
4 1 3 sylan ⊢ F ∈ Word A ∧ Fun ⁡ F -1 → F : 0 ..^ F ⟶ 1-1 A
5 4 3adant3 ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ → F : 0 ..^ F ⟶ 1-1 A
6 5 adantr ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ ∧ G = F cyclShift S → F : 0 ..^ F ⟶ 1-1 A
7 simpl3 ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ ∧ G = F cyclShift S → S ∈ ℤ
8 simpr ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ ∧ G = F cyclShift S → G = F cyclShift S
9 cshf1 ⊢ F : 0 ..^ F ⟶ 1-1 A ∧ S ∈ ℤ ∧ G = F cyclShift S → G : 0 ..^ F ⟶ 1-1 A
10 6 7 8 9 syl3anc ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ ∧ G = F cyclShift S → G : 0 ..^ F ⟶ 1-1 A
11 10 ex ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ → G = F cyclShift S → G : 0 ..^ F ⟶ 1-1 A
12 df-f1 ⊢ G : 0 ..^ F ⟶ 1-1 A ↔ G : 0 ..^ F ⟶ A ∧ Fun ⁡ G -1
13 12 simprbi ⊢ G : 0 ..^ F ⟶ 1-1 A → Fun ⁡ G -1
14 11 13 syl6 ⊢ F ∈ Word A ∧ Fun ⁡ F -1 ∧ S ∈ ℤ → G = F cyclShift S → Fun ⁡ G -1