2cshw

Description: Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018) (Revised by AV, 4-Jun-2018) (Revised by AV, 31-Oct-2018)

		Ref	Expression
	Assertion	2cshw	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (W cyclShift M) cyclShift N = W cyclShift (M + N)$

Proof

Step	Hyp	Ref	Expression
1		cshwlen	$⊢ (W \in Word V \land M \in ℤ) \to \|W cyclShift M\| = \|W\|$
2	1	3adant3	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \|W cyclShift M\| = \|W\|$
3		cshwcl	$⊢ W \in Word V \to W cyclShift M \in Word V$
4		cshwlen	$⊢ (W cyclShift M \in Word V \land N \in ℤ) \to \|(W cyclShift M) cyclShift N\| = \|W cyclShift M\|$
5	3 4	sylan	$⊢ (W \in Word V \land N \in ℤ) \to \|(W cyclShift M) cyclShift N\| = \|W cyclShift M\|$
6	5	3adant2	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \|(W cyclShift M) cyclShift N\| = \|W cyclShift M\|$
7		simp1	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to W \in Word V$
8		zaddcl	$⊢ (M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
9	8	3adant1	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to M + N \in ℤ$
10		cshwlen	$⊢ (W \in Word V \land M + N \in ℤ) \to \|W cyclShift (M + N)\| = \|W\|$
11	7 9 10	syl2anc	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \|W cyclShift (M + N)\| = \|W\|$
12	2 6 11	3eqtr4d	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \|(W cyclShift M) cyclShift N\| = \|W cyclShift (M + N)\|$
13	6 2	eqtrd	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \|(W cyclShift M) cyclShift N\| = \|W\|$
14	13	oveq2d	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (0 ..^\|(W cyclShift M) cyclShift N\|) = (0 ..^\|W\|)$
15	14	eleq2d	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (i \in (0 ..^\|(W cyclShift M) cyclShift N\|) \leftrightarrow i \in (0 ..^\|W\|))$
16	3	3ad2ant1	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to W cyclShift M \in Word V$
17	16	adantr	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to W cyclShift M \in Word V$
18		simpl3	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to N \in ℤ$
19	2	oveq2d	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (0 ..^\|W cyclShift M\|) = (0 ..^\|W\|)$
20	19	eleq2d	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (i \in (0 ..^\|W cyclShift M\|) \leftrightarrow i \in (0 ..^\|W\|))$
21	20	biimpar	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to i \in (0 ..^\|W cyclShift M\|)$
22		cshwidxmod	$⊢ (W cyclShift M \in Word V \land N \in ℤ \land i \in (0 ..^\|W cyclShift M\|)) \to ((W cyclShift M) cyclShift N) (i) = (W cyclShift M) ((i + N) \mod \|W cyclShift M\|)$
23	17 18 21 22	syl3anc	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to ((W cyclShift M) cyclShift N) (i) = (W cyclShift M) ((i + N) \mod \|W cyclShift M\|)$
24		simpl1	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to W \in Word V$
25		simpl2	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to M \in ℤ$
26		elfzo0	$⊢ i \in (0 ..^\|W\|) \leftrightarrow (i \in ℕ_{0} \land \|W\| \in ℕ \land i < \|W\|)$
27		nn0z	$⊢ i \in ℕ_{0} \to i \in ℤ$
28	27	ad2antrr	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (W \in Word V \land M \in ℤ \land N \in ℤ)) \to i \in ℤ$
29		simpr3	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (W \in Word V \land M \in ℤ \land N \in ℤ)) \to N \in ℤ$
30	28 29	zaddcld	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (W \in Word V \land M \in ℤ \land N \in ℤ)) \to i + N \in ℤ$
31		simplr	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (W \in Word V \land M \in ℤ \land N \in ℤ)) \to \|W\| \in ℕ$
32	30 31	jca	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (W \in Word V \land M \in ℤ \land N \in ℤ)) \to (i + N \in ℤ \land \|W\| \in ℕ)$
33	32	ex	$⊢ (i \in ℕ_{0} \land \|W\| \in ℕ) \to ((W \in Word V \land M \in ℤ \land N \in ℤ) \to (i + N \in ℤ \land \|W\| \in ℕ))$
34	33	3adant3	$⊢ (i \in ℕ_{0} \land \|W\| \in ℕ \land i < \|W\|) \to ((W \in Word V \land M \in ℤ \land N \in ℤ) \to (i + N \in ℤ \land \|W\| \in ℕ))$
35	26 34	sylbi	$⊢ i \in (0 ..^\|W\|) \to ((W \in Word V \land M \in ℤ \land N \in ℤ) \to (i + N \in ℤ \land \|W\| \in ℕ))$
36	35	impcom	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (i + N \in ℤ \land \|W\| \in ℕ)$
37		zmodfzo	$⊢ (i + N \in ℤ \land \|W\| \in ℕ) \to (i + N) \mod \|W\| \in (0 ..^\|W\|)$
38	36 37	syl	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|W\| \in (0 ..^\|W\|)$
39	1	oveq2d	$⊢ (W \in Word V \land M \in ℤ) \to (i + N) \mod \|W cyclShift M\| = (i + N) \mod \|W\|$
40	39	eleq1d	$⊢ (W \in Word V \land M \in ℤ) \to ((i + N) \mod \|W cyclShift M\| \in (0 ..^\|W\|) \leftrightarrow (i + N) \mod \|W\| \in (0 ..^\|W\|))$
41	40	3adant3	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to ((i + N) \mod \|W cyclShift M\| \in (0 ..^\|W\|) \leftrightarrow (i + N) \mod \|W\| \in (0 ..^\|W\|))$
42	41	adantr	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to ((i + N) \mod \|W cyclShift M\| \in (0 ..^\|W\|) \leftrightarrow (i + N) \mod \|W\| \in (0 ..^\|W\|))$
43	38 42	mpbird	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|W cyclShift M\| \in (0 ..^\|W\|)$
44		cshwidxmod	$⊢ (W \in Word V \land M \in ℤ \land (i + N) \mod \|W cyclShift M\| \in (0 ..^\|W\|)) \to (W cyclShift M) ((i + N) \mod \|W cyclShift M\|) = W ((((i + N) \mod \|W cyclShift M\|) + M) \mod \|W\|)$
45	24 25 43 44	syl3anc	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (W cyclShift M) ((i + N) \mod \|W cyclShift M\|) = W ((((i + N) \mod \|W cyclShift M\|) + M) \mod \|W\|)$
46		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
47	46	ad2antrr	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to i \in ℝ$
48		zre	$⊢ N \in ℤ \to N \in ℝ$
49	48	ad2antll	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to N \in ℝ$
50	47 49	readdcld	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to i + N \in ℝ$
51		zre	$⊢ M \in ℤ \to M \in ℝ$
52	51	ad2antrl	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to M \in ℝ$
53		nnrp	$⊢ \|W\| \in ℕ \to \|W\| \in ℝ^{+}$
54	53	ad2antlr	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to \|W\| \in ℝ^{+}$
55		modaddmod	$⊢ (i + N \in ℝ \land M \in ℝ \land \|W\| \in ℝ^{+}) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + N + M) \mod \|W\|$
56	50 52 54 55	syl3anc	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + N + M) \mod \|W\|$
57		nn0cn	$⊢ i \in ℕ_{0} \to i \in ℂ$
58	57	ad2antrr	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to i \in ℂ$
59		zcn	$⊢ M \in ℤ \to M \in ℂ$
60	59	ad2antrl	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to M \in ℂ$
61		zcn	$⊢ N \in ℤ \to N \in ℂ$
62	61	ad2antll	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to N \in ℂ$
63		add32r	$⊢ (i \in ℂ \land M \in ℂ \land N \in ℂ) \to i + M + N = i + N + M$
64	58 60 62 63	syl3anc	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to i + M + N = i + N + M$
65	64	oveq1d	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to (i + M + N) \mod \|W\| = (i + N + M) \mod \|W\|$
66	56 65	eqtr4d	$⊢ ((i \in ℕ_{0} \land \|W\| \in ℕ) \land (M \in ℤ \land N \in ℤ)) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|$
67	66	ex	$⊢ (i \in ℕ_{0} \land \|W\| \in ℕ) \to ((M \in ℤ \land N \in ℤ) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|)$
68	67	3adant3	$⊢ (i \in ℕ_{0} \land \|W\| \in ℕ \land i < \|W\|) \to ((M \in ℤ \land N \in ℤ) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|)$
69	26 68	sylbi	$⊢ i \in (0 ..^\|W\|) \to ((M \in ℤ \land N \in ℤ) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|)$
70	69	impcom	$⊢ ((M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|$
71	70	3adantl1	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (((i + N) \mod \|W\|) + M) \mod \|W\| = (i + M + N) \mod \|W\|$
72	71	fveq2d	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to W ((((i + N) \mod \|W\|) + M) \mod \|W\|) = W ((i + M + N) \mod \|W\|)$
73	2	adantr	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to \|W cyclShift M\| = \|W\|$
74	73	oveq2d	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (i + N) \mod \|W cyclShift M\| = (i + N) \mod \|W\|$
75	74	oveq1d	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to ((i + N) \mod \|W cyclShift M\|) + M = ((i + N) \mod \|W\|) + M$
76	75	fvoveq1d	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to W ((((i + N) \mod \|W cyclShift M\|) + M) \mod \|W\|) = W ((((i + N) \mod \|W\|) + M) \mod \|W\|)$
77	9	adantr	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to M + N \in ℤ$
78		simpr	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to i \in (0 ..^\|W\|)$
79		cshwidxmod	$⊢ (W \in Word V \land M + N \in ℤ \land i \in (0 ..^\|W\|)) \to (W cyclShift (M + N)) (i) = W ((i + M + N) \mod \|W\|)$
80	24 77 78 79	syl3anc	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to (W cyclShift (M + N)) (i) = W ((i + M + N) \mod \|W\|)$
81	72 76 80	3eqtr4d	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to W ((((i + N) \mod \|W cyclShift M\|) + M) \mod \|W\|) = (W cyclShift (M + N)) (i)$
82	23 45 81	3eqtrd	$⊢ ((W \in Word V \land M \in ℤ \land N \in ℤ) \land i \in (0 ..^\|W\|)) \to ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i)$
83	82	ex	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (i \in (0 ..^\|W\|) \to ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i))$
84	15 83	sylbid	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (i \in (0 ..^\|(W cyclShift M) cyclShift N\|) \to ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i))$
85	84	ralrimiv	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to \forall i \in (0 ..^\|(W cyclShift M) cyclShift N\|) ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i)$
86		cshwcl	$⊢ W cyclShift M \in Word V \to (W cyclShift M) cyclShift N \in Word V$
87	3 86	syl	$⊢ W \in Word V \to (W cyclShift M) cyclShift N \in Word V$
88		cshwcl	$⊢ W \in Word V \to W cyclShift (M + N) \in Word V$
89		eqwrd	$⊢ ((W cyclShift M) cyclShift N \in Word V \land W cyclShift (M + N) \in Word V) \to ((W cyclShift M) cyclShift N = W cyclShift (M + N) \leftrightarrow (\|(W cyclShift M) cyclShift N\| = \|W cyclShift (M + N)\| \land \forall i \in (0 ..^\|(W cyclShift M) cyclShift N\|) ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i)))$
90	87 88 89	syl2anc	$⊢ W \in Word V \to ((W cyclShift M) cyclShift N = W cyclShift (M + N) \leftrightarrow (\|(W cyclShift M) cyclShift N\| = \|W cyclShift (M + N)\| \land \forall i \in (0 ..^\|(W cyclShift M) cyclShift N\|) ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i)))$
91	90	3ad2ant1	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to ((W cyclShift M) cyclShift N = W cyclShift (M + N) \leftrightarrow (\|(W cyclShift M) cyclShift N\| = \|W cyclShift (M + N)\| \land \forall i \in (0 ..^\|(W cyclShift M) cyclShift N\|) ((W cyclShift M) cyclShift N) (i) = (W cyclShift (M + N)) (i)))$
92	12 85 91	mpbir2and	$⊢ (W \in Word V \land M \in ℤ \land N \in ℤ) \to (W cyclShift M) cyclShift N = W cyclShift (M + N)$

Metamath Proof Explorer

Theorem 2cshw

Proof