cshwcsh2id

Description: A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr and erclwwlkntr . (Contributed by AV, 9-Apr-2018) (Revised by AV, 11-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

	Ref	Expression
Hypotheses	cshwcsh2id.1	$⊢ φ \to z \in Word V$
	cshwcsh2id.2	$⊢ φ \to (\|y\| = \|z\| \land \|x\| = \|y\|)$
Assertion	cshwcsh2id	$⊢ φ \to (((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$

Proof

Step	Hyp	Ref	Expression
1		cshwcsh2id.1	$⊢ φ \to z \in Word V$
2		cshwcsh2id.2	$⊢ φ \to (\|y\| = \|z\| \land \|x\| = \|y\|)$
3		oveq1	$⊢ y = z cyclShift k \to y cyclShift m = (z cyclShift k) cyclShift m$
4	3	eqeq2d	$⊢ y = z cyclShift k \to (x = y cyclShift m \leftrightarrow x = (z cyclShift k) cyclShift m)$
5	4	anbi2d	$⊢ y = z cyclShift k \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \leftrightarrow (m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m))$
6	5	adantr	$⊢ (y = z cyclShift k \land k \in (0 \dots \|z\|)) \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \leftrightarrow (m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m))$
7		elfznn0	$⊢ k \in (0 \dots \|z\|) \to k \in ℕ_{0}$
8		elfznn0	$⊢ m \in (0 \dots \|y\|) \to m \in ℕ_{0}$
9		nn0addcl	$⊢ (k \in ℕ_{0} \land m \in ℕ_{0}) \to k + m \in ℕ_{0}$
10	7 8 9	syl2anr	$⊢ (m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m \in ℕ_{0}$
11	10	adantr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to k + m \in ℕ_{0}$
12		elfz3nn0	$⊢ k \in (0 \dots \|z\|) \to \|z\| \in ℕ_{0}$
13	12	ad2antlr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to \|z\| \in ℕ_{0}$
14		simprl	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to k + m \leq \|z\|$
15		elfz2nn0	$⊢ k + m \in (0 \dots \|z\|) \leftrightarrow (k + m \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k + m \leq \|z\|)$
16	11 13 14 15	syl3anbrc	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to k + m \in (0 \dots \|z\|)$
17	16	adantr	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to k + m \in (0 \dots \|z\|)$
18	1	adantl	$⊢ (k + m \leq \|z\| \land φ) \to z \in Word V$
19	18	adantl	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to z \in Word V$
20		elfzelz	$⊢ k \in (0 \dots \|z\|) \to k \in ℤ$
21	20	ad2antlr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to k \in ℤ$
22		elfzelz	$⊢ m \in (0 \dots \|y\|) \to m \in ℤ$
23	22	adantr	$⊢ (m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to m \in ℤ$
24	23	adantr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to m \in ℤ$
25		2cshw	$⊢ (z \in Word V \land k \in ℤ \land m \in ℤ) \to (z cyclShift k) cyclShift m = z cyclShift (k + m)$
26	19 21 24 25	syl3anc	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to (z cyclShift k) cyclShift m = z cyclShift (k + m)$
27	26	eqeq2d	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \to (x = (z cyclShift k) cyclShift m \leftrightarrow x = z cyclShift (k + m))$
28	27	biimpa	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to x = z cyclShift (k + m)$
29	17 28	jca	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))$
30	29	exp41	$⊢ m \in (0 \dots \|y\|) \to (k \in (0 \dots \|z\|) \to ((k + m \leq \|z\| \land φ) \to (x = (z cyclShift k) cyclShift m \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m)))))$
31	30	com23	$⊢ m \in (0 \dots \|y\|) \to ((k + m \leq \|z\| \land φ) \to (k \in (0 \dots \|z\|) \to (x = (z cyclShift k) cyclShift m \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m)))))$
32	31	com24	$⊢ m \in (0 \dots \|y\|) \to (x = (z cyclShift k) cyclShift m \to (k \in (0 \dots \|z\|) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m)))))$
33	32	imp	$⊢ (m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m) \to (k \in (0 \dots \|z\|) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))))$
34	33	com12	$⊢ k \in (0 \dots \|z\|) \to ((m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))))$
35	34	adantl	$⊢ (y = z cyclShift k \land k \in (0 \dots \|z\|)) \to ((m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))))$
36	6 35	sylbid	$⊢ (y = z cyclShift k \land k \in (0 \dots \|z\|)) \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))))$
37	36	ancoms	$⊢ (k \in (0 \dots \|z\|) \land y = z cyclShift k) \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m))))$
38	37	impcom	$⊢ ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to ((k + m \leq \|z\| \land φ) \to (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m)))$
39		oveq2	$⊢ n = k + m \to z cyclShift n = z cyclShift (k + m)$
40	39	rspceeqv	$⊢ (k + m \in (0 \dots \|z\|) \land x = z cyclShift (k + m)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n$
41	38 40	syl6com	$⊢ (k + m \leq \|z\| \land φ) \to (((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
42		elfz2	$⊢ k \in (0 \dots \|z\|) \leftrightarrow ((0 \in ℤ \land \|z\| \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq \|z\|))$
43		nn0z	$⊢ m \in ℕ_{0} \to m \in ℤ$
44		zaddcl	$⊢ (k \in ℤ \land m \in ℤ) \to k + m \in ℤ$
45	44	ex	$⊢ k \in ℤ \to (m \in ℤ \to k + m \in ℤ)$
46	45	adantl	$⊢ (\|z\| \in ℤ \land k \in ℤ) \to (m \in ℤ \to k + m \in ℤ)$
47	46	impcom	$⊢ (m \in ℤ \land (\|z\| \in ℤ \land k \in ℤ)) \to k + m \in ℤ$
48		simprl	$⊢ (m \in ℤ \land (\|z\| \in ℤ \land k \in ℤ)) \to \|z\| \in ℤ$
49	47 48	zsubcld	$⊢ (m \in ℤ \land (\|z\| \in ℤ \land k \in ℤ)) \to k + m - \|z\| \in ℤ$
50	49	ex	$⊢ m \in ℤ \to ((\|z\| \in ℤ \land k \in ℤ) \to k + m - \|z\| \in ℤ)$
51	43 50	syl	$⊢ m \in ℕ_{0} \to ((\|z\| \in ℤ \land k \in ℤ) \to k + m - \|z\| \in ℤ)$
52	51	com12	$⊢ (\|z\| \in ℤ \land k \in ℤ) \to (m \in ℕ_{0} \to k + m - \|z\| \in ℤ)$
53	52	3adant1	$⊢ (0 \in ℤ \land \|z\| \in ℤ \land k \in ℤ) \to (m \in ℕ_{0} \to k + m - \|z\| \in ℤ)$
54	53	adantr	$⊢ ((0 \in ℤ \land \|z\| \in ℤ \land k \in ℤ) \land (0 \leq k \land k \leq \|z\|)) \to (m \in ℕ_{0} \to k + m - \|z\| \in ℤ)$
55	42 54	sylbi	$⊢ k \in (0 \dots \|z\|) \to (m \in ℕ_{0} \to k + m - \|z\| \in ℤ)$
56	8 55	mpan9	$⊢ (m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \in ℤ$
57	56	adantr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k + m - \|z\| \in ℤ$
58		elfz2nn0	$⊢ k \in (0 \dots \|z\|) \leftrightarrow (k \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k \leq \|z\|)$
59		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
60		nn0re	$⊢ \|z\| \in ℕ_{0} \to \|z\| \in ℝ$
61	59 60	anim12i	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \to (k \in ℝ \land \|z\| \in ℝ)$
62		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
63	61 62	anim12i	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ)$
64		simplr	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to \|z\| \in ℝ$
65		readdcl	$⊢ (k \in ℝ \land m \in ℝ) \to k + m \in ℝ$
66	65	adantlr	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to k + m \in ℝ$
67	64 66	ltnled	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to (\|z\| < k + m \leftrightarrow \neg k + m \leq \|z\|)$
68	64 66	posdifd	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to (\|z\| < k + m \leftrightarrow 0 < k + m - \|z\|)$
69	68	biimpd	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to (\|z\| < k + m \to 0 < k + m - \|z\|)$
70	67 69	sylbird	$⊢ ((k \in ℝ \land \|z\| \in ℝ) \land m \in ℝ) \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|)$
71	63 70	syl	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|)$
72	71	ex	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \to (m \in ℕ_{0} \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|))$
73	72	3adant3	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k \leq \|z\|) \to (m \in ℕ_{0} \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|))$
74	58 73	sylbi	$⊢ k \in (0 \dots \|z\|) \to (m \in ℕ_{0} \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|))$
75	8 74	mpan9	$⊢ (m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to (\neg k + m \leq \|z\| \to 0 < k + m - \|z\|)$
76	75	com12	$⊢ \neg k + m \leq \|z\| \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to 0 < k + m - \|z\|)$
77	76	adantr	$⊢ (\neg k + m \leq \|z\| \land φ) \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to 0 < k + m - \|z\|)$
78	77	impcom	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to 0 < k + m - \|z\|$
79		elnnz	$⊢ k + m - \|z\| \in ℕ \leftrightarrow (k + m - \|z\| \in ℤ \land 0 < k + m - \|z\|)$
80	57 78 79	sylanbrc	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k + m - \|z\| \in ℕ$
81	80	nnnn0d	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k + m - \|z\| \in ℕ_{0}$
82	12	ad2antlr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to \|z\| \in ℕ_{0}$
83		oveq2	$⊢ \|y\| = \|z\| \to (0 \dots \|y\|) = (0 \dots \|z\|)$
84	83	eleq2d	$⊢ \|y\| = \|z\| \to (m \in (0 \dots \|y\|) \leftrightarrow m \in (0 \dots \|z\|))$
85	84	anbi1d	$⊢ \|y\| = \|z\| \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \leftrightarrow (m \in (0 \dots \|z\|) \land k \in (0 \dots \|z\|)))$
86		elfz2nn0	$⊢ m \in (0 \dots \|z\|) \leftrightarrow (m \in ℕ_{0} \land \|z\| \in ℕ_{0} \land m \leq \|z\|)$
87	59	adantr	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \to k \in ℝ$
88	87 62	anim12i	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to (k \in ℝ \land m \in ℝ)$
89	60 60	jca	$⊢ \|z\| \in ℕ_{0} \to (\|z\| \in ℝ \land \|z\| \in ℝ)$
90	89	ad2antlr	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to (\|z\| \in ℝ \land \|z\| \in ℝ)$
91		le2add	$⊢ ((k \in ℝ \land m \in ℝ) \land (\|z\| \in ℝ \land \|z\| \in ℝ)) \to ((k \leq \|z\| \land m \leq \|z\|) \to k + m \leq \|z\| + \|z\|)$
92	88 90 91	syl2anc	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to ((k \leq \|z\| \land m \leq \|z\|) \to k + m \leq \|z\| + \|z\|)$
93		nn0readdcl	$⊢ (k \in ℕ_{0} \land m \in ℕ_{0}) \to k + m \in ℝ$
94	93	adantlr	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to k + m \in ℝ$
95	60	ad2antlr	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to \|z\| \in ℝ$
96	94 95 95	lesubadd2d	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to (k + m - \|z\| \leq \|z\| \leftrightarrow k + m \leq \|z\| + \|z\|)$
97	92 96	sylibrd	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to ((k \leq \|z\| \land m \leq \|z\|) \to k + m - \|z\| \leq \|z\|)$
98	97	expcomd	$⊢ ((k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \land m \in ℕ_{0}) \to (m \leq \|z\| \to (k \leq \|z\| \to k + m - \|z\| \leq \|z\|))$
99	98	ex	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \to (m \in ℕ_{0} \to (m \leq \|z\| \to (k \leq \|z\| \to k + m - \|z\| \leq \|z\|)))$
100	99	com24	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0}) \to (k \leq \|z\| \to (m \leq \|z\| \to (m \in ℕ_{0} \to k + m - \|z\| \leq \|z\|)))$
101	100	3impia	$⊢ (k \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k \leq \|z\|) \to (m \leq \|z\| \to (m \in ℕ_{0} \to k + m - \|z\| \leq \|z\|))$
102	101	com13	$⊢ m \in ℕ_{0} \to (m \leq \|z\| \to ((k \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k \leq \|z\|) \to k + m - \|z\| \leq \|z\|))$
103	102	imp	$⊢ (m \in ℕ_{0} \land m \leq \|z\|) \to ((k \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k \leq \|z\|) \to k + m - \|z\| \leq \|z\|)$
104	58 103	biimtrid	$⊢ (m \in ℕ_{0} \land m \leq \|z\|) \to (k \in (0 \dots \|z\|) \to k + m - \|z\| \leq \|z\|)$
105	104	3adant2	$⊢ (m \in ℕ_{0} \land \|z\| \in ℕ_{0} \land m \leq \|z\|) \to (k \in (0 \dots \|z\|) \to k + m - \|z\| \leq \|z\|)$
106	86 105	sylbi	$⊢ m \in (0 \dots \|z\|) \to (k \in (0 \dots \|z\|) \to k + m - \|z\| \leq \|z\|)$
107	106	imp	$⊢ (m \in (0 \dots \|z\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \leq \|z\|$
108	85 107	biimtrdi	$⊢ \|y\| = \|z\| \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \leq \|z\|)$
109	108	adantr	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \leq \|z\|)$
110	2 109	syl	$⊢ φ \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \leq \|z\|)$
111	110	adantl	$⊢ (\neg k + m \leq \|z\| \land φ) \to ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m - \|z\| \leq \|z\|)$
112	111	impcom	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k + m - \|z\| \leq \|z\|$
113		elfz2nn0	$⊢ k + m - \|z\| \in (0 \dots \|z\|) \leftrightarrow (k + m - \|z\| \in ℕ_{0} \land \|z\| \in ℕ_{0} \land k + m - \|z\| \leq \|z\|)$
114	81 82 112 113	syl3anbrc	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k + m - \|z\| \in (0 \dots \|z\|)$
115	114	adantr	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to k + m - \|z\| \in (0 \dots \|z\|)$
116	1	adantl	$⊢ (\neg k + m \leq \|z\| \land φ) \to z \in Word V$
117	116	adantl	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to z \in Word V$
118	20	ad2antlr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to k \in ℤ$
119	23	adantr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to m \in ℤ$
120	117 118 119 25	syl3anc	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to (z cyclShift k) cyclShift m = z cyclShift (k + m)$
121	20 22 44	syl2anr	$⊢ (m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \to k + m \in ℤ$
122		cshwsublen	$⊢ (z \in Word V \land k + m \in ℤ) \to z cyclShift (k + m) = z cyclShift (k + m - \|z\|)$
123	116 121 122	syl2anr	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to z cyclShift (k + m) = z cyclShift (k + m - \|z\|)$
124	120 123	eqtrd	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to (z cyclShift k) cyclShift m = z cyclShift (k + m - \|z\|)$
125	124	eqeq2d	$⊢ ((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \to (x = (z cyclShift k) cyclShift m \leftrightarrow x = z cyclShift (k + m - \|z\|))$
126	125	biimpa	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to x = z cyclShift (k + m - \|z\|)$
127	115 126	jca	$⊢ (((m \in (0 \dots \|y\|) \land k \in (0 \dots \|z\|)) \land (\neg k + m \leq \|z\| \land φ)) \land x = (z cyclShift k) cyclShift m) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|))$
128	127	exp41	$⊢ m \in (0 \dots \|y\|) \to (k \in (0 \dots \|z\|) \to ((\neg k + m \leq \|z\| \land φ) \to (x = (z cyclShift k) cyclShift m \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))))$
129	128	com23	$⊢ m \in (0 \dots \|y\|) \to ((\neg k + m \leq \|z\| \land φ) \to (k \in (0 \dots \|z\|) \to (x = (z cyclShift k) cyclShift m \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))))$
130	129	com24	$⊢ m \in (0 \dots \|y\|) \to (x = (z cyclShift k) cyclShift m \to (k \in (0 \dots \|z\|) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))))$
131	130	imp	$⊢ (m \in (0 \dots \|y\|) \land x = (z cyclShift k) cyclShift m) \to (k \in (0 \dots \|z\|) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|))))$
132	5 131	biimtrdi	$⊢ y = z cyclShift k \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to (k \in (0 \dots \|z\|) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))))$
133	132	com23	$⊢ y = z cyclShift k \to (k \in (0 \dots \|z\|) \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))))$
134	133	impcom	$⊢ (k \in (0 \dots \|z\|) \land y = z cyclShift k) \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|))))$
135	134	impcom	$⊢ ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to ((\neg k + m \leq \|z\| \land φ) \to (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)))$
136		oveq2	$⊢ n = k + m - \|z\| \to z cyclShift n = z cyclShift (k + m - \|z\|)$
137	136	rspceeqv	$⊢ (k + m - \|z\| \in (0 \dots \|z\|) \land x = z cyclShift (k + m - \|z\|)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n$
138	135 137	syl6com	$⊢ (\neg k + m \leq \|z\| \land φ) \to (((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
139	41 138	pm2.61ian	$⊢ φ \to (((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$

Metamath Proof Explorer

Theorem cshwcsh2id

Proof