cshword

Description: Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018) (Revised by AV, 12-Oct-2022)

		Ref	Expression
	Assertion	cshword	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$

Proof

Step	Hyp	Ref	Expression
1		iswrd	$⊢ W \in Word V \leftrightarrow \exists l \in ℕ_{0} W : (0 ..^l) ⟶ V$
2		ffn	$⊢ W : (0 ..^l) ⟶ V \to W Fn (0 ..^l)$
3	2	reximi	$⊢ \exists l \in ℕ_{0} W : (0 ..^l) ⟶ V \to \exists l \in ℕ_{0} W Fn (0 ..^l)$
4	1 3	sylbi	$⊢ W \in Word V \to \exists l \in ℕ_{0} W Fn (0 ..^l)$
5		fneq1	$⊢ w = W \to (w Fn (0 ..^l) \leftrightarrow W Fn (0 ..^l))$
6	5	rexbidv	$⊢ w = W \to (\exists l \in ℕ_{0} w Fn (0 ..^l) \leftrightarrow \exists l \in ℕ_{0} W Fn (0 ..^l))$
7	6	elabg	$⊢ W \in Word V \to (W \in \{w \| \exists l \in ℕ_{0} w Fn (0 ..^l)\} \leftrightarrow \exists l \in ℕ_{0} W Fn (0 ..^l))$
8	4 7	mpbird	$⊢ W \in Word V \to W \in \{w \| \exists l \in ℕ_{0} w Fn (0 ..^l)\}$
9		cshfn	$⊢ (W \in \{w \| \exists l \in ℕ_{0} w Fn (0 ..^l)\} \land N \in ℤ) \to W cyclShift N = if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)))$
10	8 9	sylan	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)))$
11		iftrue	$⊢ W = \emptyset \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = \emptyset$
12	11	adantr	$⊢ (W = \emptyset \land (W \in Word V \land N \in ℤ)) \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = \emptyset$
13		oveq1	$⊢ W = \emptyset \to W substr ⟨N \mod \|W\|, \|W\|⟩ = \emptyset substr ⟨N \mod \|W\|, \|W\|⟩$
14		swrd0	$⊢ \emptyset substr ⟨N \mod \|W\|, \|W\|⟩ = \emptyset$
15	13 14	eqtrdi	$⊢ W = \emptyset \to W substr ⟨N \mod \|W\|, \|W\|⟩ = \emptyset$
16		oveq1	$⊢ W = \emptyset \to W prefix (N \mod \|W\|) = \emptyset prefix (N \mod \|W\|)$
17		pfx0	$⊢ \emptyset prefix (N \mod \|W\|) = \emptyset$
18	16 17	eqtrdi	$⊢ W = \emptyset \to W prefix (N \mod \|W\|) = \emptyset$
19	15 18	oveq12d	$⊢ W = \emptyset \to (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)) = \emptyset ++ \emptyset$
20	19	adantr	$⊢ (W = \emptyset \land (W \in Word V \land N \in ℤ)) \to (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|)) = \emptyset ++ \emptyset$
21		ccatidid	$⊢ \emptyset ++ \emptyset = \emptyset$
22	20 21	eqtr2di	$⊢ (W = \emptyset \land (W \in Word V \land N \in ℤ)) \to \emptyset = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
23	12 22	eqtrd	$⊢ (W = \emptyset \land (W \in Word V \land N \in ℤ)) \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
24		iffalse	$⊢ \neg W = \emptyset \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
25	24	adantr	$⊢ (\neg W = \emptyset \land (W \in Word V \land N \in ℤ)) \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
26	23 25	pm2.61ian	$⊢ (W \in Word V \land N \in ℤ) \to if (W = \emptyset, \emptyset, (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))) = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$
27	10 26	eqtrd	$⊢ (W \in Word V \land N \in ℤ) \to W cyclShift N = (W substr ⟨N \mod \|W\|, \|W\|⟩) ++ (W prefix (N \mod \|W\|))$

Metamath Proof Explorer

Theorem cshword

Proof