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 𝑛 ) } )