# 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 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left\{{y}\in \mathrm{Word}{V}|\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right\}=\left\{{y}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right\}$

### Proof

Step Hyp Ref Expression
1 lencl ${⊢}{X}\in \mathrm{Word}{V}\to \left|{X}\right|\in {ℕ}_{0}$
2 elnn0uz ${⊢}\left|{X}\right|\in {ℕ}_{0}↔\left|{X}\right|\in {ℤ}_{\ge 0}$
3 1 2 sylib ${⊢}{X}\in \mathrm{Word}{V}\to \left|{X}\right|\in {ℤ}_{\ge 0}$
4 3 adantr ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {N}=\left|{X}\right|\right)\to \left|{X}\right|\in {ℤ}_{\ge 0}$
5 eleq1 ${⊢}{N}=\left|{X}\right|\to \left({N}\in {ℤ}_{\ge 0}↔\left|{X}\right|\in {ℤ}_{\ge 0}\right)$
6 5 adantl ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {N}=\left|{X}\right|\right)\to \left({N}\in {ℤ}_{\ge 0}↔\left|{X}\right|\in {ℤ}_{\ge 0}\right)$
7 4 6 mpbird ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {N}=\left|{X}\right|\right)\to {N}\in {ℤ}_{\ge 0}$
8 7 3adant2 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {N}\in {ℤ}_{\ge 0}$
9 8 adantr ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to {N}\in {ℤ}_{\ge 0}$
10 fzisfzounsn ${⊢}{N}\in {ℤ}_{\ge 0}\to \left(0\dots {N}\right)=\left(0..^{N}\right)\cup \left\{{N}\right\}$
11 9 10 syl ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(0\dots {N}\right)=\left(0..^{N}\right)\cup \left\{{N}\right\}$
12 11 rexeqdv ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔\exists {n}\in \left(\left(0..^{N}\right)\cup \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
13 rexun ${⊢}\exists {n}\in \left(\left(0..^{N}\right)\cup \left\{{N}\right\}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔\left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\vee \exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
14 12 13 syl6bb ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔\left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\vee \exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)\right)$
15 fvex ${⊢}\left|{X}\right|\in \mathrm{V}$
16 eleq1 ${⊢}{N}=\left|{X}\right|\to \left({N}\in \mathrm{V}↔\left|{X}\right|\in \mathrm{V}\right)$
17 15 16 mpbiri ${⊢}{N}=\left|{X}\right|\to {N}\in \mathrm{V}$
18 oveq2 ${⊢}{n}={N}\to {X}\mathrm{cyclShift}{n}={X}\mathrm{cyclShift}{N}$
19 18 eqeq2d ${⊢}{n}={N}\to \left({y}={X}\mathrm{cyclShift}{n}↔{y}={X}\mathrm{cyclShift}{N}\right)$
20 19 rexsng ${⊢}{N}\in \mathrm{V}\to \left(\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔{y}={X}\mathrm{cyclShift}{N}\right)$
21 17 20 syl ${⊢}{N}=\left|{X}\right|\to \left(\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔{y}={X}\mathrm{cyclShift}{N}\right)$
22 21 3ad2ant3 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left(\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔{y}={X}\mathrm{cyclShift}{N}\right)$
23 22 adantr ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔{y}={X}\mathrm{cyclShift}{N}\right)$
24 oveq2 ${⊢}{N}=\left|{X}\right|\to {X}\mathrm{cyclShift}{N}={X}\mathrm{cyclShift}\left|{X}\right|$
25 24 3ad2ant3 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {X}\mathrm{cyclShift}{N}={X}\mathrm{cyclShift}\left|{X}\right|$
26 cshwn ${⊢}{X}\in \mathrm{Word}{V}\to {X}\mathrm{cyclShift}\left|{X}\right|={X}$
27 26 3ad2ant1 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {X}\mathrm{cyclShift}\left|{X}\right|={X}$
28 25 27 eqtrd ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {X}\mathrm{cyclShift}{N}={X}$
29 28 eqeq2d ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left({y}={X}\mathrm{cyclShift}{N}↔{y}={X}\right)$
30 29 adantr ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left({y}={X}\mathrm{cyclShift}{N}↔{y}={X}\right)$
31 cshw0 ${⊢}{X}\in \mathrm{Word}{V}\to {X}\mathrm{cyclShift}0={X}$
32 31 3ad2ant1 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {X}\mathrm{cyclShift}0={X}$
33 lennncl ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \right)\to \left|{X}\right|\in ℕ$
34 33 3adant3 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left|{X}\right|\in ℕ$
35 eleq1 ${⊢}{N}=\left|{X}\right|\to \left({N}\in ℕ↔\left|{X}\right|\in ℕ\right)$
36 35 3ad2ant3 ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left({N}\in ℕ↔\left|{X}\right|\in ℕ\right)$
37 34 36 mpbird ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to {N}\in ℕ$
38 lbfzo0 ${⊢}0\in \left(0..^{N}\right)↔{N}\in ℕ$
39 37 38 sylibr ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to 0\in \left(0..^{N}\right)$
40 oveq2 ${⊢}0={n}\to {X}\mathrm{cyclShift}0={X}\mathrm{cyclShift}{n}$
41 40 eqeq1d ${⊢}0={n}\to \left({X}\mathrm{cyclShift}0={X}↔{X}\mathrm{cyclShift}{n}={X}\right)$
42 41 eqcoms ${⊢}{n}=0\to \left({X}\mathrm{cyclShift}0={X}↔{X}\mathrm{cyclShift}{n}={X}\right)$
43 eqcom ${⊢}{X}\mathrm{cyclShift}{n}={X}↔{X}={X}\mathrm{cyclShift}{n}$
44 42 43 syl6bb ${⊢}{n}=0\to \left({X}\mathrm{cyclShift}0={X}↔{X}={X}\mathrm{cyclShift}{n}\right)$
45 44 adantl ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {n}=0\right)\to \left({X}\mathrm{cyclShift}0={X}↔{X}={X}\mathrm{cyclShift}{n}\right)$
46 45 biimpd ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {n}=0\right)\to \left({X}\mathrm{cyclShift}0={X}\to {X}={X}\mathrm{cyclShift}{n}\right)$
47 39 46 rspcimedv ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left({X}\mathrm{cyclShift}0={X}\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{X}={X}\mathrm{cyclShift}{n}\right)$
48 32 47 mpd ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{X}={X}\mathrm{cyclShift}{n}$
49 48 adantr ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{X}={X}\mathrm{cyclShift}{n}$
50 49 adantr ${⊢}\left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\wedge {y}={X}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{X}={X}\mathrm{cyclShift}{n}$
51 eqeq1 ${⊢}{y}={X}\to \left({y}={X}\mathrm{cyclShift}{n}↔{X}={X}\mathrm{cyclShift}{n}\right)$
52 51 adantl ${⊢}\left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\wedge {y}={X}\right)\to \left({y}={X}\mathrm{cyclShift}{n}↔{X}={X}\mathrm{cyclShift}{n}\right)$
53 52 rexbidv ${⊢}\left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\wedge {y}={X}\right)\to \left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{X}={X}\mathrm{cyclShift}{n}\right)$
54 50 53 mpbird ${⊢}\left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\wedge {y}={X}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}$
55 54 ex ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left({y}={X}\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
56 30 55 sylbid ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left({y}={X}\mathrm{cyclShift}{N}\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
57 23 56 sylbid ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
58 57 com12 ${⊢}\exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\to \left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
59 58 jao1i ${⊢}\left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\vee \exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)\to \left(\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
60 59 com12 ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\vee \exists {n}\in \left\{{N}\right\}\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
61 14 60 sylbid ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\to \exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
62 fzossfz ${⊢}\left(0..^{N}\right)\subseteq \left(0\dots {N}\right)$
63 ssrexv ${⊢}\left(0..^{N}\right)\subseteq \left(0\dots {N}\right)\to \left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
64 62 63 mp1i ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\to \exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
65 61 64 impbid ${⊢}\left(\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\wedge {y}\in \mathrm{Word}{V}\right)\to \left(\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}↔\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right)$
66 65 rabbidva ${⊢}\left({X}\in \mathrm{Word}{V}\wedge {X}\ne \varnothing \wedge {N}=\left|{X}\right|\right)\to \left\{{y}\in \mathrm{Word}{V}|\exists {n}\in \left(0\dots {N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right\}=\left\{{y}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^{N}\right)\phantom{\rule{.4em}{0ex}}{y}={X}\mathrm{cyclShift}{n}\right\}$