cshweqdif2

Description: If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018) (Revised by AV, 6-Jun-2018) (Revised by AV, 1-Nov-2018)

		Ref	Expression
	Assertion	cshweqdif2	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (W cyclShift N = U cyclShift M \to U cyclShift (M - N) = W)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (W \in Word V \land U \in Word V) \to U \in Word V$
2	1	adantr	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to U \in Word V$
3		zsubcl	$⊢ (M \in ℤ \land N \in ℤ) \to M - N \in ℤ$
4	3	ancoms	$⊢ (N \in ℤ \land M \in ℤ) \to M - N \in ℤ$
5	4	adantl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to M - N \in ℤ$
6		simpr	$⊢ (N \in ℤ \land M \in ℤ) \to M \in ℤ$
7	6	adantl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to M \in ℤ$
8	2 5 7	3jca	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (U \in Word V \land M - N \in ℤ \land M \in ℤ)$
9	8	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (U \in Word V \land M - N \in ℤ \land M \in ℤ)$
10		3cshw	$⊢ (U \in Word V \land M - N \in ℤ \land M \in ℤ) \to U cyclShift (M - N) = ((U cyclShift M) cyclShift (M - N)) cyclShift (\|U\| - M)$
11	9 10	syl	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to U cyclShift (M - N) = ((U cyclShift M) cyclShift (M - N)) cyclShift (\|U\| - M)$
12		simpl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (W \in Word V \land U \in Word V)$
13	12	ancomd	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (U \in Word V \land W \in Word V)$
14	13	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (U \in Word V \land W \in Word V)$
15		simpr	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (N \in ℤ \land M \in ℤ)$
16	15	ancomd	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (M \in ℤ \land N \in ℤ)$
17	16	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (M \in ℤ \land N \in ℤ)$
18		simpr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to W cyclShift N = U cyclShift M$
19	18	eqcomd	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to U cyclShift M = W cyclShift N$
20		cshwleneq	$⊢ ((U \in Word V \land W \in Word V) \land (M \in ℤ \land N \in ℤ) \land U cyclShift M = W cyclShift N) \to \|U\| = \|W\|$
21	14 17 19 20	syl3anc	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to \|U\| = \|W\|$
22	21	oveq1d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to \|U\| - M = \|W\| - M$
23	22	oveq2d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to ((U cyclShift M) cyclShift (M - N)) cyclShift (\|U\| - M) = ((U cyclShift M) cyclShift (M - N)) cyclShift (\|W\| - M)$
24	11 23	eqtrd	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to U cyclShift (M - N) = ((U cyclShift M) cyclShift (M - N)) cyclShift (\|W\| - M)$
25	19	oveq1d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (U cyclShift M) cyclShift (M - N) = (W cyclShift N) cyclShift (M - N)$
26		simpl	$⊢ (W \in Word V \land U \in Word V) \to W \in Word V$
27	26	adantr	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to W \in Word V$
28		simpl	$⊢ (N \in ℤ \land M \in ℤ) \to N \in ℤ$
29	28	adantl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to N \in ℤ$
30	27 29 5	3jca	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (W \in Word V \land N \in ℤ \land M - N \in ℤ)$
31	30	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (W \in Word V \land N \in ℤ \land M - N \in ℤ)$
32		2cshw	$⊢ (W \in Word V \land N \in ℤ \land M - N \in ℤ) \to (W cyclShift N) cyclShift (M - N) = W cyclShift (N + M - N)$
33	31 32	syl	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (W cyclShift N) cyclShift (M - N) = W cyclShift (N + M - N)$
34		zcn	$⊢ N \in ℤ \to N \in ℂ$
35		zcn	$⊢ M \in ℤ \to M \in ℂ$
36	34 35	anim12i	$⊢ (N \in ℤ \land M \in ℤ) \to (N \in ℂ \land M \in ℂ)$
37	36	adantl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (N \in ℂ \land M \in ℂ)$
38	37	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (N \in ℂ \land M \in ℂ)$
39		pncan3	$⊢ (N \in ℂ \land M \in ℂ) \to N + M - N = M$
40	38 39	syl	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to N + M - N = M$
41	40	oveq2d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to W cyclShift (N + M - N) = W cyclShift M$
42	25 33 41	3eqtrd	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (U cyclShift M) cyclShift (M - N) = W cyclShift M$
43	42	oveq1d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to ((U cyclShift M) cyclShift (M - N)) cyclShift (\|W\| - M) = (W cyclShift M) cyclShift (\|W\| - M)$
44		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
45	44	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
46	45	adantr	$⊢ (W \in Word V \land U \in Word V) \to \|W\| \in ℤ$
47		zsubcl	$⊢ (\|W\| \in ℤ \land M \in ℤ) \to \|W\| - M \in ℤ$
48	46 6 47	syl2an	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to \|W\| - M \in ℤ$
49	27 7 48	3jca	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (W \in Word V \land M \in ℤ \land \|W\| - M \in ℤ)$
50	49	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (W \in Word V \land M \in ℤ \land \|W\| - M \in ℤ)$
51		2cshw	$⊢ (W \in Word V \land M \in ℤ \land \|W\| - M \in ℤ) \to (W cyclShift M) cyclShift (\|W\| - M) = W cyclShift (M + \|W\| - M)$
52	50 51	syl	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (W cyclShift M) cyclShift (\|W\| - M) = W cyclShift (M + \|W\| - M)$
53	24 43 52	3eqtrd	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to U cyclShift (M - N) = W cyclShift (M + \|W\| - M)$
54	44	nn0cnd	$⊢ W \in Word V \to \|W\| \in ℂ$
55	54	adantr	$⊢ (W \in Word V \land U \in Word V) \to \|W\| \in ℂ$
56	35	adantl	$⊢ (N \in ℤ \land M \in ℤ) \to M \in ℂ$
57	55 56	anim12i	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (\|W\| \in ℂ \land M \in ℂ)$
58	57	ancomd	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (M \in ℂ \land \|W\| \in ℂ)$
59	58	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to (M \in ℂ \land \|W\| \in ℂ)$
60		pncan3	$⊢ (M \in ℂ \land \|W\| \in ℂ) \to M + \|W\| - M = \|W\|$
61	59 60	syl	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to M + \|W\| - M = \|W\|$
62	61	oveq2d	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to W cyclShift (M + \|W\| - M) = W cyclShift \|W\|$
63		cshwn	$⊢ W \in Word V \to W cyclShift \|W\| = W$
64	27 63	syl	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to W cyclShift \|W\| = W$
65	64	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to W cyclShift \|W\| = W$
66	53 62 65	3eqtrd	$⊢ (((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \land W cyclShift N = U cyclShift M) \to U cyclShift (M - N) = W$
67	66	ex	$⊢ ((W \in Word V \land U \in Word V) \land (N \in ℤ \land M \in ℤ)) \to (W cyclShift N = U cyclShift M \to U cyclShift (M - N) = W)$

Metamath Proof Explorer

Theorem cshweqdif2

Proof