cshwrepswhash1

Description: The size of the set of (different!) words resulting by cyclically shifting a nonempty "repeated symbol word" is 1. (Contributed by AV, 18-May-2018) (Revised by AV, 8-Nov-2018)

		Ref	Expression
	Hypothesis	cshwrepswhash1.m	$⊢ M = \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\}$
	Assertion	cshwrepswhash1	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \|M\| = 1$

Proof

Step	Hyp	Ref	Expression
1		cshwrepswhash1.m	$⊢ M = \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\}$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3		repsdf2	$⊢ (A \in V \land N \in ℕ_{0}) \to (W = A repeatS N \leftrightarrow (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A))$
4	2 3	sylan2	$⊢ (A \in V \land N \in ℕ) \to (W = A repeatS N \leftrightarrow (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A))$
5		simp1	$⊢ (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to W \in Word V$
6	5	adantl	$⊢ ((A \in V \land N \in ℕ) \land (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A)) \to W \in Word V$
7		eleq1	$⊢ N = \|W\| \to (N \in ℕ \leftrightarrow \|W\| \in ℕ)$
8	7	eqcoms	$⊢ \|W\| = N \to (N \in ℕ \leftrightarrow \|W\| \in ℕ)$
9		lbfzo0	$⊢ 0 \in (0 ..^\|W\|) \leftrightarrow \|W\| \in ℕ$
10	9	biimpri	$⊢ \|W\| \in ℕ \to 0 \in (0 ..^\|W\|)$
11	8 10	syl6bi	$⊢ \|W\| = N \to (N \in ℕ \to 0 \in (0 ..^\|W\|))$
12	11	3ad2ant2	$⊢ (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to (N \in ℕ \to 0 \in (0 ..^\|W\|))$
13	12	com12	$⊢ N \in ℕ \to ((W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to 0 \in (0 ..^\|W\|))$
14	13	adantl	$⊢ (A \in V \land N \in ℕ) \to ((W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to 0 \in (0 ..^\|W\|))$
15	14	imp	$⊢ ((A \in V \land N \in ℕ) \land (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A)) \to 0 \in (0 ..^\|W\|)$
16		cshw0	$⊢ W \in Word V \to W cyclShift 0 = W$
17	6 16	syl	$⊢ ((A \in V \land N \in ℕ) \land (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A)) \to W cyclShift 0 = W$
18		oveq2	$⊢ n = 0 \to W cyclShift n = W cyclShift 0$
19	18	eqeq1d	$⊢ n = 0 \to (W cyclShift n = W \leftrightarrow W cyclShift 0 = W)$
20	19	rspcev	$⊢ (0 \in (0 ..^\|W\|) \land W cyclShift 0 = W) \to \exists n \in (0 ..^\|W\|) W cyclShift n = W$
21	15 17 20	syl2anc	$⊢ ((A \in V \land N \in ℕ) \land (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A)) \to \exists n \in (0 ..^\|W\|) W cyclShift n = W$
22		eqeq2	$⊢ w = W \to (W cyclShift n = w \leftrightarrow W cyclShift n = W)$
23	22	rexbidv	$⊢ w = W \to (\exists n \in (0 ..^\|W\|) W cyclShift n = w \leftrightarrow \exists n \in (0 ..^\|W\|) W cyclShift n = W)$
24	23	rspcev	$⊢ (W \in Word V \land \exists n \in (0 ..^\|W\|) W cyclShift n = W) \to \exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w$
25	6 21 24	syl2anc	$⊢ ((A \in V \land N \in ℕ) \land (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A)) \to \exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w$
26	25	ex	$⊢ (A \in V \land N \in ℕ) \to ((W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to \exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w)$
27	4 26	sylbid	$⊢ (A \in V \land N \in ℕ) \to (W = A repeatS N \to \exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w)$
28	27	3impia	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w$
29		repsw	$⊢ (A \in V \land N \in ℕ_{0}) \to A repeatS N \in Word V$
30	2 29	sylan2	$⊢ (A \in V \land N \in ℕ) \to A repeatS N \in Word V$
31	30	3adant3	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to A repeatS N \in Word V$
32		simpll3	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to W = A repeatS N$
33	32	oveq1d	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to W cyclShift n = (A repeatS N) cyclShift n$
34		simp1	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to A \in V$
35	34	ad2antrr	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to A \in V$
36	2	3ad2ant2	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to N \in ℕ_{0}$
37	36	ad2antrr	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to N \in ℕ_{0}$
38		elfzoelz	$⊢ n \in (0 ..^\|W\|) \to n \in ℤ$
39	38	adantl	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to n \in ℤ$
40		repswcshw	$⊢ (A \in V \land N \in ℕ_{0} \land n \in ℤ) \to (A repeatS N) cyclShift n = A repeatS N$
41	35 37 39 40	syl3anc	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to (A repeatS N) cyclShift n = A repeatS N$
42	33 41	eqtrd	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to W cyclShift n = A repeatS N$
43	42	eqeq1d	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to (W cyclShift n = u \leftrightarrow A repeatS N = u)$
44	43	biimpd	$⊢ (((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \land n \in (0 ..^\|W\|)) \to (W cyclShift n = u \to A repeatS N = u)$
45	44	rexlimdva	$⊢ ((A \in V \land N \in ℕ \land W = A repeatS N) \land u \in Word V) \to (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to A repeatS N = u)$
46	45	ralrimiva	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to A repeatS N = u)$
47		eqeq1	$⊢ w = A repeatS N \to (w = u \leftrightarrow A repeatS N = u)$
48	47	imbi2d	$⊢ w = A repeatS N \to ((\exists n \in (0 ..^\|W\|) W cyclShift n = u \to w = u) \leftrightarrow (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to A repeatS N = u))$
49	48	ralbidv	$⊢ w = A repeatS N \to (\forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to w = u) \leftrightarrow \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to A repeatS N = u))$
50	49	rspcev	$⊢ (A repeatS N \in Word V \land \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to A repeatS N = u)) \to \exists w \in Word V \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to w = u)$
51	31 46 50	syl2anc	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \exists w \in Word V \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to w = u)$
52		eqeq2	$⊢ w = u \to (W cyclShift n = w \leftrightarrow W cyclShift n = u)$
53	52	rexbidv	$⊢ w = u \to (\exists n \in (0 ..^\|W\|) W cyclShift n = w \leftrightarrow \exists n \in (0 ..^\|W\|) W cyclShift n = u)$
54	53	reu7	$⊢ \exists! w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w \leftrightarrow (\exists w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w \land \exists w \in Word V \forall u \in Word V (\exists n \in (0 ..^\|W\|) W cyclShift n = u \to w = u))$
55	28 51 54	sylanbrc	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \exists! w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w$
56		reusn	$⊢ \exists! w \in Word V \exists n \in (0 ..^\|W\|) W cyclShift n = w \leftrightarrow \exists r \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\} = \{r\}$
57	55 56	sylib	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \exists r \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\} = \{r\}$
58	1	eqeq1i	$⊢ M = \{r\} \leftrightarrow \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\} = \{r\}$
59	58	exbii	$⊢ \exists r M = \{r\} \leftrightarrow \exists r \{w \in Word V \| \exists n \in (0 ..^\|W\|) W cyclShift n = w\} = \{r\}$
60	57 59	sylibr	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \exists r M = \{r\}$
61	1	cshwsex	$⊢ W \in Word V \to M \in V$
62	61	3ad2ant1	$⊢ (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = A) \to M \in V$
63	4 62	syl6bi	$⊢ (A \in V \land N \in ℕ) \to (W = A repeatS N \to M \in V)$
64	63	3impia	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to M \in V$
65		hash1snb	$⊢ M \in V \to (\|M\| = 1 \leftrightarrow \exists r M = \{r\})$
66	64 65	syl	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to (\|M\| = 1 \leftrightarrow \exists r M = \{r\})$
67	60 66	mpbird	$⊢ (A \in V \land N \in ℕ \land W = A repeatS N) \to \|M\| = 1$

Metamath Proof Explorer

Theorem cshwrepswhash1

Proof