Metamath Proof Explorer

Theorem cshf1

Description: Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021)

Ref Expression
Assertion cshf1 ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
2 iswrdi ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 → 𝐹 ∈ Word 𝐴 )
3 1 2 syl ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → 𝐹 ∈ Word 𝐴 )
4 cshwf ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝐹 cyclShift 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
5 4 3adant1 ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝐹 cyclShift 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
6 5 adantr ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → ( 𝐹 cyclShift 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
7 feq1 ⊢ ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ↔ ( 𝐹 cyclShift 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ) )
8 7 adantl ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ↔ ( 𝐹 cyclShift 𝑆 ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ) )
9 6 8 mpbird ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 )
10 dff13 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
11 fveq1 ⊢ ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐺 ‘ 𝑖 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) )
12 11 3ad2ant1 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝐺 ‘ 𝑖 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) )
13 12 adantr ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ‘ 𝑖 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) )
14 cshwidxmod ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
15 14 3expia ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
16 15 3adant1 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
17 16 com12 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
18 17 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
19 18 impcom ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
20 13 19 eqtrd ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
21 fveq1 ⊢ ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐺 ‘ 𝑗 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) )
22 21 3ad2ant1 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝐺 ‘ 𝑗 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) )
23 22 adantr ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ‘ 𝑗 ) = ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) )
24 cshwidxmod ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
25 24 3expia ⊢ ( ( 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
26 25 3adant1 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
27 26 adantld ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
28 27 imp ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 cyclShift 𝑆 ) ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
29 23 28 eqtrd ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐺 ‘ 𝑗 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
30 20 29 eqeq12d ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ↔ ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
31 30 adantlr ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) ↔ ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
32 elfzo0 ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝐹 ) ) )
33 nn0z ⊢ ( 𝑖 ∈ ℕ0 → 𝑖 ∈ ℤ )
34 33 adantr ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → 𝑖 ∈ ℤ )
35 34 adantl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → 𝑖 ∈ ℤ )
36 simpl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → 𝑆 ∈ ℤ )
37 35 36 zaddcld ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( 𝑖 + 𝑆 ) ∈ ℤ )
38 simpr ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
39 38 adantl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
40 37 39 jca ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
41 40 ex ⊢ ( 𝑆 ∈ ℤ → ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
42 41 3ad2ant3 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
43 42 com12 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
44 43 3adant3 ⊢ ( ( 𝑖 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝑖 < ( ♯ ‘ 𝐹 ) ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
45 32 44 sylbi ⊢ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
46 45 adantr ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
47 46 impcom ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
48 zmodfzo ⊢ ( ( ( 𝑖 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
49 47 48 syl ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
50 elfzo0 ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝑗 < ( ♯ ‘ 𝐹 ) ) )
51 nn0z ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℤ )
52 51 adantr ⊢ ( ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → 𝑗 ∈ ℤ )
53 52 adantl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → 𝑗 ∈ ℤ )
54 simpl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → 𝑆 ∈ ℤ )
55 53 54 zaddcld ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( 𝑗 + 𝑆 ) ∈ ℤ )
56 simpr ⊢ ( ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
57 56 adantl ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
58 55 57 jca ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
59 58 expcom ⊢ ( ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( 𝑆 ∈ ℤ → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
60 59 3adant3 ⊢ ( ( 𝑗 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ∧ 𝑗 < ( ♯ ‘ 𝐹 ) ) → ( 𝑆 ∈ ℤ → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
61 50 60 sylbi ⊢ ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑆 ∈ ℤ → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
62 61 com12 ⊢ ( 𝑆 ∈ ℤ → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
63 62 3ad2ant3 ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
64 63 adantld ⊢ ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) ) )
65 64 imp ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) )
66 zmodfzo ⊢ ( ( ( 𝑗 + 𝑆 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ ) → ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
67 65 66 syl ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
68 fveqeq2 ⊢ ( 𝑥 = ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ 𝑦 ) ) )
69 eqeq1 ⊢ ( 𝑥 = ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( 𝑥 = 𝑦 ↔ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 𝑦 ) )
70 68 69 imbi12d ⊢ ( 𝑥 = ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 𝑦 ) ) )
71 fveq2 ⊢ ( 𝑦 = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
72 71 eqeq2d ⊢ ( 𝑦 = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
73 eqeq2 ⊢ ( 𝑦 = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 𝑦 ↔ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
74 72 73 imbi12d ⊢ ( 𝑦 = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = 𝑦 ) ↔ ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
75 70 74 rspc2v ⊢ ( ( ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
76 49 67 75 syl2anc ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) )
77 simpr ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
78 addmodlteq ⊢ ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ↔ 𝑖 = 𝑗 ) )
79 78 3expa ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑆 ∈ ℤ ) → ( ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ↔ 𝑖 = 𝑗 ) )
80 79 ancoms ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ↔ 𝑖 = 𝑗 ) )
81 80 bicomd ⊢ ( ( 𝑆 ∈ ℤ ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 = 𝑗 ↔ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
82 81 3ad2antl3 ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 = 𝑗 ↔ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
83 82 adantr ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 = 𝑗 ↔ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) )
84 77 83 sylibrd ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∧ ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → 𝑖 = 𝑗 ) )
85 84 ex ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) = ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → 𝑖 = 𝑗 ) ) )
86 76 85 syld ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → 𝑖 = 𝑗 ) ) )
87 86 impancom ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ( ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → 𝑖 = 𝑗 ) ) )
88 87 imp ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 ‘ ( ( 𝑖 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) = ( 𝐹 ‘ ( ( 𝑗 + 𝑆 ) mod ( ♯ ‘ 𝐹 ) ) ) → 𝑖 = 𝑗 ) )
89 31 88 sylbid ⊢ ( ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ∧ ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
90 89 ralrimivva ⊢ ( ( ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
91 90 3exp1 ⊢ ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐹 ∈ Word 𝐴 → ( 𝑆 ∈ ℤ → ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) )
92 91 com14 ⊢ ( ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) → ( 𝐹 ∈ Word 𝐴 → ( 𝑆 ∈ ℤ → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) )
93 92 adantl ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑦 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) → ( 𝐹 ∈ Word 𝐴 → ( 𝑆 ∈ ℤ → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) )
94 10 93 sylbi ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → ( 𝐹 ∈ Word 𝐴 → ( 𝑆 ∈ ℤ → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) )
95 94 3imp1 ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
96 9 95 jca ⊢ ( ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ) ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
97 96 3exp1 ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → ( 𝐹 ∈ Word 𝐴 → ( 𝑆 ∈ ℤ → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) ) )
98 3 97 mpd ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 → ( 𝑆 ∈ ℤ → ( 𝐺 = ( 𝐹 cyclShift 𝑆 ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) ) ) )
99 98 3imp ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
100 dff13 ⊢ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ↔ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝐴 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∀ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
101 99 100 sylibr ⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = ( 𝐹 cyclShift 𝑆 ) ) → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ 𝐴 )