cshwlen

Description: The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018) (Revised by AV, 20-May-2018) (Revised by AV, 27-Oct-2018) (Proof shortened by AV, 16-Oct-2022)

		Ref	Expression
	Assertion	cshwlen	$⊢ (W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|W\|$

Proof

Step	Hyp	Ref	Expression
1		0csh0	$⊢ \emptyset cyclShift N = \emptyset$
2		oveq1	$⊢ W = \emptyset \to W cyclShift N = \emptyset cyclShift N$
3		id	$⊢ W = \emptyset \to W = \emptyset$
4	1 2 3	3eqtr4a	$⊢ W = \emptyset \to W cyclShift N = W$
5	4	fveq2d	$⊢ W = \emptyset \to \|W cyclShift N\| = \|W\|$
6	5	a1d	$⊢ W = \emptyset \to ((W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|W\|)$
7		cshword	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
8	7	fveq2d	$⊢ (W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|(W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))\|$
9	8	adantr	$⊢ ((W \in Word V \land N \in ℤ) \land W \neq \emptyset) \to \|W cyclShift N\| = \|(W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))\|$
10		swrdcl	$⊢ W \in Word V \to W substr ⟨N \mod \|W\|, \|W\|⟩ \in Word V$
11		pfxcl	$⊢ W \in Word V \to W prefix (N \mod \|W\|) \in Word V$
12		ccatlen	$⊢ (W substr ⟨N \mod \|W\|, \|W\|⟩ \in Word V \land W prefix (N \mod \|W\|) \in Word V) \to \|(W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))\| = \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\|$
13	10 11 12	syl2anc	$⊢ W \in Word V \to \|(W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))\| = \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\|$
14	13	ad2antrr	$⊢ ((W \in Word V \land N \in ℤ) \land W \neq \emptyset) \to \|(W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))\| = \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\|$
15		lennncl	$⊢ (W \in Word V \land W \neq \emptyset) \to \|W\| \in ℕ$
16		pm3.21	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to (W \in Word V \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)))$
17	16	ex	$⊢ \|W\| \in ℕ \to (N \in ℤ \to (W \in Word V \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ))))$
18	15 17	syl	$⊢ (W \in Word V \land W \neq \emptyset) \to (N \in ℤ \to (W \in Word V \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ))))$
19	18	ex	$⊢ W \in Word V \to (W \neq \emptyset \to (N \in ℤ \to (W \in Word V \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)))))$
20	19	com24	$⊢ W \in Word V \to (W \in Word V \to (N \in ℤ \to (W \neq \emptyset \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)))))$
21	20	pm2.43i	$⊢ W \in Word V \to (N \in ℤ \to (W \neq \emptyset \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ))))$
22	21	imp31	$⊢ ((W \in Word V \land N \in ℤ) \land W \neq \emptyset) \to (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ))$
23		simpl	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to W \in Word V$
24		zmodfzp1	$⊢ (N \in ℤ \land \|W\| \in ℕ) \to N \mod \|W\| \in (0 \dots \|W\|)$
25	24	ancoms	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to N \mod \|W\| \in (0 \dots \|W\|)$
26	25	adantl	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to N \mod \|W\| \in (0 \dots \|W\|)$
27		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
28		nn0fz0	$⊢ \|W\| \in ℕ_{0} \leftrightarrow \|W\| \in (0 \dots \|W\|)$
29	27 28	sylib	$⊢ W \in Word V \to \|W\| \in (0 \dots \|W\|)$
30	29	adantr	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W\| \in (0 \dots \|W\|)$
31		swrdlen	$⊢ (W \in Word V \land N \mod \|W\| \in (0 \dots \|W\|) \land \|W\| \in (0 \dots \|W\|)) \to \|W substr ⟨N \mod \|W\|, \|W\|⟩\| = \|W\| - (N \mod \|W\|)$
32	23 26 30 31	syl3anc	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W substr ⟨N \mod \|W\|, \|W\|⟩\| = \|W\| - (N \mod \|W\|)$
33		pfxlen	$⊢ (W \in Word V \land N \mod \|W\| \in (0 \dots \|W\|)) \to \|W prefix (N \mod \|W\|)\| = N \mod \|W\|$
34	25 33	sylan2	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W prefix (N \mod \|W\|)\| = N \mod \|W\|$
35	32 34	oveq12d	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\| = \|W\| - (N \mod \|W\|) + (N \mod \|W\|)$
36	27	nn0cnd	$⊢ W \in Word V \to \|W\| \in ℂ$
37		zmodcl	$⊢ (N \in ℤ \land \|W\| \in ℕ) \to N \mod \|W\| \in ℕ_{0}$
38	37	nn0cnd	$⊢ (N \in ℤ \land \|W\| \in ℕ) \to N \mod \|W\| \in ℂ$
39	38	ancoms	$⊢ (\|W\| \in ℕ \land N \in ℤ) \to N \mod \|W\| \in ℂ$
40		npcan	$⊢ (\|W\| \in ℂ \land N \mod \|W\| \in ℂ) \to \|W\| - (N \mod \|W\|) + (N \mod \|W\|) = \|W\|$
41	36 39 40	syl2an	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W\| - (N \mod \|W\|) + (N \mod \|W\|) = \|W\|$
42	35 41	eqtrd	$⊢ (W \in Word V \land (\|W\| \in ℕ \land N \in ℤ)) \to \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\| = \|W\|$
43	22 42	syl	$⊢ ((W \in Word V \land N \in ℤ) \land W \neq \emptyset) \to \|W substr ⟨N \mod \|W\|, \|W\|⟩\| + \|W prefix (N \mod \|W\|)\| = \|W\|$
44	9 14 43	3eqtrd	$⊢ ((W \in Word V \land N \in ℤ) \land W \neq \emptyset) \to \|W cyclShift N\| = \|W\|$
45	44	expcom	$⊢ W \neq \emptyset \to ((W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|W\|)$
46	6 45	pm2.61ine	$⊢ (W \in Word V \land N \in ℤ) \to \|W cyclShift N\| = \|W\|$

Metamath Proof Explorer

Theorem cshwlen

Proof