Step |
Hyp |
Ref |
Expression |
1 |
|
cshwcshid.1 |
⊢ ( 𝜑 → 𝑦 ∈ Word 𝑉 ) |
2 |
|
cshwcshid.2 |
⊢ ( 𝜑 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) |
3 |
|
fznn0sub2 |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) |
4 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) ) |
5 |
4
|
eleq2d |
⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ↔ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) ) |
6 |
3 5
|
syl5ibr |
⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
7 |
6 2
|
syl11 |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝜑 → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( 𝜑 → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) ) |
9 |
8
|
impcom |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ) |
10 |
|
simpl |
⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑦 ∈ Word 𝑉 ) |
11 |
|
elfzelz |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → 𝑚 ∈ ℤ ) |
12 |
11
|
adantl |
⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑚 ∈ ℤ ) |
13 |
|
elfz2nn0 |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ↔ ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑦 ) ) ) |
14 |
|
nn0z |
⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ♯ ‘ 𝑦 ) ∈ ℤ ) |
15 |
|
nn0z |
⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ ) |
16 |
|
zsubcl |
⊢ ( ( ( ♯ ‘ 𝑦 ) ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) |
17 |
14 15 16
|
syl2anr |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) |
18 |
17
|
3adant3 |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) |
19 |
13 18
|
sylbi |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) |
20 |
19
|
adantl |
⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) |
21 |
10 12 20
|
3jca |
⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) ) |
22 |
1 21
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) ) |
23 |
|
2cshw |
⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ℤ ) → ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) ) |
24 |
22 23
|
syl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) ) |
25 |
|
nn0cn |
⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℂ ) |
26 |
|
nn0cn |
⊢ ( ( ♯ ‘ 𝑦 ) ∈ ℕ0 → ( ♯ ‘ 𝑦 ) ∈ ℂ ) |
27 |
25 26
|
anim12i |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) ) |
28 |
27
|
3adant3 |
⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑦 ) ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑦 ) ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) ) |
29 |
13 28
|
sylbi |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) ) |
30 |
|
pncan3 |
⊢ ( ( 𝑚 ∈ ℂ ∧ ( ♯ ‘ 𝑦 ) ∈ ℂ ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) ) |
31 |
29 30
|
syl |
⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) ) |
32 |
31
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ♯ ‘ 𝑦 ) ) |
33 |
32
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 cyclShift ( 𝑚 + ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) = ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) ) |
34 |
|
cshwn |
⊢ ( 𝑦 ∈ Word 𝑉 → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 ) |
35 |
1 34
|
syl |
⊢ ( 𝜑 → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 ) |
36 |
35
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → ( 𝑦 cyclShift ( ♯ ‘ 𝑦 ) ) = 𝑦 ) |
37 |
24 33 36
|
3eqtrrd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) → 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) |
38 |
37
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) |
39 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) |
40 |
39
|
eqeq2d |
⊢ ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) ) |
41 |
40
|
adantl |
⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) ) |
42 |
41
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ( 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ↔ 𝑦 = ( ( 𝑦 cyclShift 𝑚 ) cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) ) |
43 |
38 42
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) |
44 |
|
oveq2 |
⊢ ( 𝑛 = ( ( ♯ ‘ 𝑦 ) − 𝑚 ) → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) |
45 |
44
|
rspceeqv |
⊢ ( ( ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) ∧ 𝑦 = ( 𝑥 cyclShift ( ( ♯ ‘ 𝑦 ) − 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) |
46 |
9 43 45
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) |
47 |
46
|
ex |
⊢ ( 𝜑 → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) |