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	$⊢ (X \in Word V \land X \neq \emptyset \land N = \|X\|) \to \{y \in Word V \| \exists n \in (0 \dots N) y = X cyclShift n\} = \{y \in Word V \| \exists n \in (0 ..^N) y = X cyclShift n\}$

Proof

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

Metamath Proof Explorer

Theorem scshwfzeqfzo

Proof