cshw0

Description: A word cyclically shifted by 0 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	cshw0	$⊢ W \in Word V \to W cyclShift 0 = W$

Proof

Step	Hyp	Ref	Expression
1		0csh0	$⊢ \emptyset cyclShift 0 = \emptyset$
2		oveq1	$⊢ \emptyset = W \to \emptyset cyclShift 0 = W cyclShift 0$
3		id	$⊢ \emptyset = W \to \emptyset = W$
4	1 2 3	3eqtr3a	$⊢ \emptyset = W \to W cyclShift 0 = W$
5	4	a1d	$⊢ \emptyset = W \to (W \in Word V \to W cyclShift 0 = W)$
6		0z	$⊢ 0 \in ℤ$
7		cshword	$⊢ (W \in Word V \land 0 \in ℤ) \to W cyclShift 0 = (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|))$
8	6 7	mpan2	$⊢ W \in Word V \to W cyclShift 0 = (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|))$
9	8	adantr	$⊢ (W \in Word V \land \emptyset \neq W) \to W cyclShift 0 = (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|))$
10		necom	$⊢ \emptyset \neq W \leftrightarrow W \neq \emptyset$
11		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
12		nnrp	$⊢ \|W\| \in ℕ \to \|W\| \in ℝ^{+}$
13		0mod	$⊢ \|W\| \in ℝ^{+} \to 0 \mod \|W\| = 0$
14	13	opeq1d	$⊢ \|W\| \in ℝ^{+} \to ⟨0 \mod \|W\|, \|W\|⟩ = ⟨0, \|W\|⟩$
15	14	oveq2d	$⊢ \|W\| \in ℝ^{+} \to W substr ⟨0 \mod \|W\|, \|W\|⟩ = W substr ⟨0, \|W\|⟩$
16	13	oveq2d	$⊢ \|W\| \in ℝ^{+} \to W prefix (0 \mod \|W\|) = W prefix 0$
17	15 16	oveq12d	$⊢ \|W\| \in ℝ^{+} \to (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|)) = (W substr ⟨0, \|W\|⟩) ++ (W prefix 0)$
18	11 12 17	3syl	$⊢ (W \in Word V \land W \neq \emptyset) \to (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|)) = (W substr ⟨0, \|W\|⟩) ++ (W prefix 0)$
19	10 18	sylan2b	$⊢ (W \in Word V \land \emptyset \neq W) \to (W substr ⟨0 \mod \|W\|, \|W\|⟩) ++ (W prefix (0 \mod \|W\|)) = (W substr ⟨0, \|W\|⟩) ++ (W prefix 0)$
20	9 19	eqtrd	$⊢ (W \in Word V \land \emptyset \neq W) \to W cyclShift 0 = (W substr ⟨0, \|W\|⟩) ++ (W prefix 0)$
21		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
22		pfxval	$⊢ (W \in Word V \land \|W\| \in ℕ_{0}) \to W prefix \|W\| = W substr ⟨0, \|W\|⟩$
23	21 22	mpdan	$⊢ W \in Word V \to W prefix \|W\| = W substr ⟨0, \|W\|⟩$
24		pfxid	$⊢ W \in Word V \to W prefix \|W\| = W$
25	23 24	eqtr3d	$⊢ W \in Word V \to W substr ⟨0, \|W\|⟩ = W$
26	25	adantr	$⊢ (W \in Word V \land \emptyset \neq W) \to W substr ⟨0, \|W\|⟩ = W$
27		pfx00	$⊢ W prefix 0 = \emptyset$
28	27	a1i	$⊢ (W \in Word V \land \emptyset \neq W) \to W prefix 0 = \emptyset$
29	26 28	oveq12d	$⊢ (W \in Word V \land \emptyset \neq W) \to (W substr ⟨0, \|W\|⟩) ++ (W prefix 0) = W ++ \emptyset$
30		ccatrid	$⊢ W \in Word V \to W ++ \emptyset = W$
31	30	adantr	$⊢ (W \in Word V \land \emptyset \neq W) \to W ++ \emptyset = W$
32	20 29 31	3eqtrd	$⊢ (W \in Word V \land \emptyset \neq W) \to W cyclShift 0 = W$
33	32	expcom	$⊢ \emptyset \neq W \to (W \in Word V \to W cyclShift 0 = W)$
34	5 33	pm2.61ine	$⊢ W \in Word V \to W cyclShift 0 = W$

Metamath Proof Explorer

Theorem cshw0

Proof