cshwcshid

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

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

Proof

Step	Hyp	Ref	Expression
1		cshwcshid.1	$⊢ φ \to y \in Word V$
2		cshwcshid.2	$⊢ φ \to \|x\| = \|y\|$
3		fznn0sub2	$⊢ m \in (0 \dots \|y\|) \to \|y\| - m \in (0 \dots \|y\|)$
4		oveq2	$⊢ \|x\| = \|y\| \to (0 \dots \|x\|) = (0 \dots \|y\|)$
5	4	eleq2d	$⊢ \|x\| = \|y\| \to (\|y\| - m \in (0 \dots \|x\|) \leftrightarrow \|y\| - m \in (0 \dots \|y\|))$
6	3 5	syl5ibr	$⊢ \|x\| = \|y\| \to (m \in (0 \dots \|y\|) \to \|y\| - m \in (0 \dots \|x\|))$
7	6 2	syl11	$⊢ m \in (0 \dots \|y\|) \to (φ \to \|y\| - m \in (0 \dots \|x\|))$
8	7	adantr	$⊢ (m \in (0 \dots \|y\|) \land x = y cyclShift m) \to (φ \to \|y\| - m \in (0 \dots \|x\|))$
9	8	impcom	$⊢ (φ \land (m \in (0 \dots \|y\|) \land x = y cyclShift m)) \to \|y\| - m \in (0 \dots \|x\|)$
10		simpl	$⊢ (y \in Word V \land m \in (0 \dots \|y\|)) \to y \in Word V$
11		elfzelz	$⊢ m \in (0 \dots \|y\|) \to m \in ℤ$
12	11	adantl	$⊢ (y \in Word V \land m \in (0 \dots \|y\|)) \to m \in ℤ$
13		elfz2nn0	$⊢ m \in (0 \dots \|y\|) \leftrightarrow (m \in ℕ_{0} \land \|y\| \in ℕ_{0} \land m \leq \|y\|)$
14		nn0z	$⊢ \|y\| \in ℕ_{0} \to \|y\| \in ℤ$
15		nn0z	$⊢ m \in ℕ_{0} \to m \in ℤ$
16		zsubcl	$⊢ (\|y\| \in ℤ \land m \in ℤ) \to \|y\| - m \in ℤ$
17	14 15 16	syl2anr	$⊢ (m \in ℕ_{0} \land \|y\| \in ℕ_{0}) \to \|y\| - m \in ℤ$
18	17	3adant3	$⊢ (m \in ℕ_{0} \land \|y\| \in ℕ_{0} \land m \leq \|y\|) \to \|y\| - m \in ℤ$
19	13 18	sylbi	$⊢ m \in (0 \dots \|y\|) \to \|y\| - m \in ℤ$
20	19	adantl	$⊢ (y \in Word V \land m \in (0 \dots \|y\|)) \to \|y\| - m \in ℤ$
21	10 12 20	3jca	$⊢ (y \in Word V \land m \in (0 \dots \|y\|)) \to (y \in Word V \land m \in ℤ \land \|y\| - m \in ℤ)$
22	1 21	sylan	$⊢ (φ \land m \in (0 \dots \|y\|)) \to (y \in Word V \land m \in ℤ \land \|y\| - m \in ℤ)$
23		2cshw	$⊢ (y \in Word V \land m \in ℤ \land \|y\| - m \in ℤ) \to (y cyclShift m) cyclShift (\|y\| - m) = y cyclShift (m + \|y\| - m)$
24	22 23	syl	$⊢ (φ \land m \in (0 \dots \|y\|)) \to (y cyclShift m) cyclShift (\|y\| - m) = y cyclShift (m + \|y\| - m)$
25		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
26		nn0cn	$⊢ \|y\| \in ℕ_{0} \to \|y\| \in ℂ$
27	25 26	anim12i	$⊢ (m \in ℕ_{0} \land \|y\| \in ℕ_{0}) \to (m \in ℂ \land \|y\| \in ℂ)$
28	27	3adant3	$⊢ (m \in ℕ_{0} \land \|y\| \in ℕ_{0} \land m \leq \|y\|) \to (m \in ℂ \land \|y\| \in ℂ)$
29	13 28	sylbi	$⊢ m \in (0 \dots \|y\|) \to (m \in ℂ \land \|y\| \in ℂ)$
30		pncan3	$⊢ (m \in ℂ \land \|y\| \in ℂ) \to m + \|y\| - m = \|y\|$
31	29 30	syl	$⊢ m \in (0 \dots \|y\|) \to m + \|y\| - m = \|y\|$
32	31	adantl	$⊢ (φ \land m \in (0 \dots \|y\|)) \to m + \|y\| - m = \|y\|$
33	32	oveq2d	$⊢ (φ \land m \in (0 \dots \|y\|)) \to y cyclShift (m + \|y\| - m) = y cyclShift \|y\|$
34		cshwn	$⊢ y \in Word V \to y cyclShift \|y\| = y$
35	1 34	syl	$⊢ φ \to y cyclShift \|y\| = y$
36	35	adantr	$⊢ (φ \land m \in (0 \dots \|y\|)) \to y cyclShift \|y\| = y$
37	24 33 36	3eqtrrd	$⊢ (φ \land m \in (0 \dots \|y\|)) \to y = (y cyclShift m) cyclShift (\|y\| - m)$
38	37	adantrr	$⊢ (φ \land (m \in (0 \dots \|y\|) \land x = y cyclShift m)) \to y = (y cyclShift m) cyclShift (\|y\| - m)$
39		oveq1	$⊢ x = y cyclShift m \to x cyclShift (\|y\| - m) = (y cyclShift m) cyclShift (\|y\| - m)$
40	39	eqeq2d	$⊢ x = y cyclShift m \to (y = x cyclShift (\|y\| - m) \leftrightarrow y = (y cyclShift m) cyclShift (\|y\| - m))$
41	40	adantl	$⊢ (m \in (0 \dots \|y\|) \land x = y cyclShift m) \to (y = x cyclShift (\|y\| - m) \leftrightarrow y = (y cyclShift m) cyclShift (\|y\| - m))$
42	41	adantl	$⊢ (φ \land (m \in (0 \dots \|y\|) \land x = y cyclShift m)) \to (y = x cyclShift (\|y\| - m) \leftrightarrow y = (y cyclShift m) cyclShift (\|y\| - m))$
43	38 42	mpbird	$⊢ (φ \land (m \in (0 \dots \|y\|) \land x = y cyclShift m)) \to y = x cyclShift (\|y\| - m)$
44		oveq2	$⊢ n = \|y\| - m \to x cyclShift n = x cyclShift (\|y\| - m)$
45	44	rspceeqv	$⊢ (\|y\| - m \in (0 \dots \|x\|) \land y = x cyclShift (\|y\| - m)) \to \exists n \in (0 \dots \|x\|) y = x cyclShift n$
46	9 43 45	syl2anc	$⊢ (φ \land (m \in (0 \dots \|y\|) \land x = y cyclShift m)) \to \exists n \in (0 \dots \|x\|) y = x cyclShift n$
47	46	ex	$⊢ φ \to ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \to \exists n \in (0 \dots \|x\|) y = x cyclShift n)$

Metamath Proof Explorer

Theorem cshwcshid

Proof