Metamath Proof Explorer


Theorem scshwfzeqfzo

Description: For a nonempty word the sets of shifted words, expressd by a finite interval of integers or by a half-open integer range are identical. (Contributed by Alexander van der Vekens, 15-Jun-2018)

Ref Expression
Assertion scshwfzeqfzo ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → { 𝑦 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) } = { 𝑦 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) } )

Proof

Step Hyp Ref Expression
1 lencl ( 𝑋 ∈ Word 𝑉 → ( ♯ ‘ 𝑋 ) ∈ ℕ0 )
2 elnn0uz ( ( ♯ ‘ 𝑋 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) )
3 1 2 sylib ( 𝑋 ∈ Word 𝑉 → ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) )
4 3 adantr ( ( 𝑋 ∈ Word 𝑉𝑁 = ( ♯ ‘ 𝑋 ) ) → ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) )
5 eleq1 ( 𝑁 = ( ♯ ‘ 𝑋 ) → ( 𝑁 ∈ ( ℤ ‘ 0 ) ↔ ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) ) )
6 5 adantl ( ( 𝑋 ∈ Word 𝑉𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑁 ∈ ( ℤ ‘ 0 ) ↔ ( ♯ ‘ 𝑋 ) ∈ ( ℤ ‘ 0 ) ) )
7 4 6 mpbird ( ( 𝑋 ∈ Word 𝑉𝑁 = ( ♯ ‘ 𝑋 ) ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
8 7 3adant2 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
9 8 adantr ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → 𝑁 ∈ ( ℤ ‘ 0 ) )
10 fzisfzounsn ( 𝑁 ∈ ( ℤ ‘ 0 ) → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
11 9 10 syl ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( 0 ... 𝑁 ) = ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) )
12 11 rexeqdv ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
13 rexun ( ∃ 𝑛 ∈ ( ( 0 ..^ 𝑁 ) ∪ { 𝑁 } ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ∨ ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
14 12 13 bitrdi ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ∨ ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) ) )
15 fvex ( ♯ ‘ 𝑋 ) ∈ V
16 eleq1 ( 𝑁 = ( ♯ ‘ 𝑋 ) → ( 𝑁 ∈ V ↔ ( ♯ ‘ 𝑋 ) ∈ V ) )
17 15 16 mpbiri ( 𝑁 = ( ♯ ‘ 𝑋 ) → 𝑁 ∈ V )
18 oveq2 ( 𝑛 = 𝑁 → ( 𝑋 cyclShift 𝑛 ) = ( 𝑋 cyclShift 𝑁 ) )
19 18 eqeq2d ( 𝑛 = 𝑁 → ( 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑋 cyclShift 𝑁 ) ) )
20 19 rexsng ( 𝑁 ∈ V → ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑋 cyclShift 𝑁 ) ) )
21 17 20 syl ( 𝑁 = ( ♯ ‘ 𝑋 ) → ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑋 cyclShift 𝑁 ) ) )
22 21 3ad2ant3 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑋 cyclShift 𝑁 ) ) )
23 22 adantr ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑋 cyclShift 𝑁 ) ) )
24 oveq2 ( 𝑁 = ( ♯ ‘ 𝑋 ) → ( 𝑋 cyclShift 𝑁 ) = ( 𝑋 cyclShift ( ♯ ‘ 𝑋 ) ) )
25 24 3ad2ant3 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑋 cyclShift 𝑁 ) = ( 𝑋 cyclShift ( ♯ ‘ 𝑋 ) ) )
26 cshwn ( 𝑋 ∈ Word 𝑉 → ( 𝑋 cyclShift ( ♯ ‘ 𝑋 ) ) = 𝑋 )
27 26 3ad2ant1 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑋 cyclShift ( ♯ ‘ 𝑋 ) ) = 𝑋 )
28 25 27 eqtrd ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑋 cyclShift 𝑁 ) = 𝑋 )
29 28 eqeq2d ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑦 = ( 𝑋 cyclShift 𝑁 ) ↔ 𝑦 = 𝑋 ) )
30 29 adantr ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( 𝑦 = ( 𝑋 cyclShift 𝑁 ) ↔ 𝑦 = 𝑋 ) )
31 cshw0 ( 𝑋 ∈ Word 𝑉 → ( 𝑋 cyclShift 0 ) = 𝑋 )
32 31 3ad2ant1 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑋 cyclShift 0 ) = 𝑋 )
33 lennncl ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
34 33 3adant3 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( ♯ ‘ 𝑋 ) ∈ ℕ )
35 eleq1 ( 𝑁 = ( ♯ ‘ 𝑋 ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ ) )
36 35 3ad2ant3 ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( 𝑁 ∈ ℕ ↔ ( ♯ ‘ 𝑋 ) ∈ ℕ ) )
37 34 36 mpbird ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → 𝑁 ∈ ℕ )
38 lbfzo0 ( 0 ∈ ( 0 ..^ 𝑁 ) ↔ 𝑁 ∈ ℕ )
39 37 38 sylibr ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → 0 ∈ ( 0 ..^ 𝑁 ) )
40 oveq2 ( 0 = 𝑛 → ( 𝑋 cyclShift 0 ) = ( 𝑋 cyclShift 𝑛 ) )
41 40 eqeq1d ( 0 = 𝑛 → ( ( 𝑋 cyclShift 0 ) = 𝑋 ↔ ( 𝑋 cyclShift 𝑛 ) = 𝑋 ) )
42 41 eqcoms ( 𝑛 = 0 → ( ( 𝑋 cyclShift 0 ) = 𝑋 ↔ ( 𝑋 cyclShift 𝑛 ) = 𝑋 ) )
43 eqcom ( ( 𝑋 cyclShift 𝑛 ) = 𝑋𝑋 = ( 𝑋 cyclShift 𝑛 ) )
44 42 43 bitrdi ( 𝑛 = 0 → ( ( 𝑋 cyclShift 0 ) = 𝑋𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
45 44 adantl ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑛 = 0 ) → ( ( 𝑋 cyclShift 0 ) = 𝑋𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
46 45 biimpd ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑛 = 0 ) → ( ( 𝑋 cyclShift 0 ) = 𝑋𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
47 39 46 rspcimedv ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ( ( 𝑋 cyclShift 0 ) = 𝑋 → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
48 32 47 mpd ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ( 𝑋 cyclShift 𝑛 ) )
49 48 adantr ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ( 𝑋 cyclShift 𝑛 ) )
50 49 adantr ( ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) ∧ 𝑦 = 𝑋 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ( 𝑋 cyclShift 𝑛 ) )
51 eqeq1 ( 𝑦 = 𝑋 → ( 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
52 51 adantl ( ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) ∧ 𝑦 = 𝑋 ) → ( 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ 𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
53 52 rexbidv ( ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) ∧ 𝑦 = 𝑋 ) → ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 = ( 𝑋 cyclShift 𝑛 ) ) )
54 50 53 mpbird ( ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) ∧ 𝑦 = 𝑋 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) )
55 54 ex ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( 𝑦 = 𝑋 → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
56 30 55 sylbid ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( 𝑦 = ( 𝑋 cyclShift 𝑁 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
57 23 56 sylbid ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
58 57 com12 ( ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) → ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
59 58 jao1i ( ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ∨ ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) → ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
60 59 com12 ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ∨ ∃ 𝑛 ∈ { 𝑁 } 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
61 14 60 sylbid ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
62 fzossfz ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
63 ssrexv ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 ) → ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
64 62 63 mp1i ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
65 61 64 impbid ( ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) ∧ 𝑦 ∈ Word 𝑉 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) ) )
66 65 rabbidva ( ( 𝑋 ∈ Word 𝑉𝑋 ≠ ∅ ∧ 𝑁 = ( ♯ ‘ 𝑋 ) ) → { 𝑦 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) } = { 𝑦 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑦 = ( 𝑋 cyclShift 𝑛 ) } )