cshwn

Description: A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 26-Oct-2018)

		Ref	Expression
	Assertion	cshwn	$⊢ W \in Word V \to W cyclShift \|W\| = W$

Proof

Step	Hyp	Ref	Expression
1		0csh0	$⊢ \emptyset cyclShift \|W\| = \emptyset$
2		oveq1	$⊢ \emptyset = W \to \emptyset cyclShift \|W\| = W cyclShift \|W\|$
3		id	$⊢ \emptyset = W \to \emptyset = W$
4	1 2 3	3eqtr3a	$⊢ \emptyset = W \to W cyclShift \|W\| = W$
5	4	a1d	$⊢ \emptyset = W \to (W \in Word V \to W cyclShift \|W\| = W)$
6		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
7	6	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
8		cshwmodn	$⊢ (W \in Word V \land \|W\| \in ℤ) \to W cyclShift \|W\| = W cyclShift (\|W\| \mod \|W\|)$
9	7 8	mpdan	$⊢ W \in Word V \to W cyclShift \|W\| = W cyclShift (\|W\| \mod \|W\|)$
10	9	adantl	$⊢ (\emptyset \neq W \land W \in Word V) \to W cyclShift \|W\| = W cyclShift (\|W\| \mod \|W\|)$
11		necom	$⊢ \emptyset \neq W \leftrightarrow W \neq \emptyset$
12		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
13	11 12	sylan2b	$⊢ (W \in Word V \land \emptyset \neq W) \to \|W\| \in ℕ$
14	13	nnrpd	$⊢ (W \in Word V \land \emptyset \neq W) \to \|W\| \in ℝ^{+}$
15	14	ancoms	$⊢ (\emptyset \neq W \land W \in Word V) \to \|W\| \in ℝ^{+}$
16		modid0	$⊢ \|W\| \in ℝ^{+} \to \|W\| \mod \|W\| = 0$
17	15 16	syl	$⊢ (\emptyset \neq W \land W \in Word V) \to \|W\| \mod \|W\| = 0$
18	17	oveq2d	$⊢ (\emptyset \neq W \land W \in Word V) \to W cyclShift (\|W\| \mod \|W\|) = W cyclShift 0$
19		cshw0	$⊢ W \in Word V \to W cyclShift 0 = W$
20	19	adantl	$⊢ (\emptyset \neq W \land W \in Word V) \to W cyclShift 0 = W$
21	10 18 20	3eqtrd	$⊢ (\emptyset \neq W \land W \in Word V) \to W cyclShift \|W\| = W$
22	21	ex	$⊢ \emptyset \neq W \to (W \in Word V \to W cyclShift \|W\| = W)$
23	5 22	pm2.61ine	$⊢ W \in Word V \to W cyclShift \|W\| = W$

Metamath Proof Explorer

Theorem cshwn

Proof