cshimadifsn0

Description: The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021)

		Ref	Expression
	Assertion	cshimadifsn0	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$

Proof

Step	Hyp	Ref	Expression
1		cshimadifsn	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift J) [(1 ..^N)]$
2		elfzoel2	$⊢ J \in (0 ..^N) \to N \in ℤ$
3		elfzom1elp1fzo1	$⊢ (N \in ℤ \land y \in (0 ..^N - 1)) \to y + 1 \in (1 ..^N)$
4	3	ex	$⊢ N \in ℤ \to (y \in (0 ..^N - 1) \to y + 1 \in (1 ..^N))$
5	2 4	syl	$⊢ J \in (0 ..^N) \to (y \in (0 ..^N - 1) \to y + 1 \in (1 ..^N))$
6	5	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (y \in (0 ..^N - 1) \to y + 1 \in (1 ..^N))$
7	6	imp	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y + 1 \in (1 ..^N)$
8		elfzo1elm1fzo0	$⊢ x \in (1 ..^N) \to x - 1 \in (0 ..^N - 1)$
9	8	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in (1 ..^N)) \to x - 1 \in (0 ..^N - 1)$
10		oveq1	$⊢ y = x - 1 \to y + 1 = x - 1 + 1$
11	10	eqeq2d	$⊢ y = x - 1 \to (x = y + 1 \leftrightarrow x = x - 1 + 1)$
12	11	adantl	$⊢ (((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in (1 ..^N)) \land y = x - 1) \to (x = y + 1 \leftrightarrow x = x - 1 + 1)$
13		elfzoelz	$⊢ x \in (1 ..^N) \to x \in ℤ$
14	13	zcnd	$⊢ x \in (1 ..^N) \to x \in ℂ$
15		npcan1	$⊢ x \in ℂ \to x - 1 + 1 = x$
16	14 15	syl	$⊢ x \in (1 ..^N) \to x - 1 + 1 = x$
17	16	eqcomd	$⊢ x \in (1 ..^N) \to x = x - 1 + 1$
18	17	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in (1 ..^N)) \to x = x - 1 + 1$
19	9 12 18	rspcedvd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in (1 ..^N)) \to \exists y \in (0 ..^N - 1) x = y + 1$
20		fveq2	$⊢ x = y + 1 \to (F cyclShift J) (x) = (F cyclShift J) (y + 1)$
21	20	3ad2ant3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1) \land x = y + 1) \to (F cyclShift J) (x) = (F cyclShift J) (y + 1)$
22		elfzoelz	$⊢ y \in (0 ..^N - 1) \to y \in ℤ$
23	22	zcnd	$⊢ y \in (0 ..^N - 1) \to y \in ℂ$
24	23	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y \in ℂ$
25		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
26	25	zcnd	$⊢ J \in (0 ..^N) \to J \in ℂ$
27	26	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to J \in ℂ$
28	27	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to J \in ℂ$
29		1cnd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to 1 \in ℂ$
30		add32r	$⊢ (y \in ℂ \land J \in ℂ \land 1 \in ℂ) \to y + J + 1 = y + 1 + J$
31	24 28 29 30	syl3anc	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y + J + 1 = y + 1 + J$
32	31	fvoveq1d	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to F ((y + J + 1) \mod \|F\|) = F ((y + 1 + J) \mod \|F\|)$
33		simpl1	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to F \in Word S$
34	25	peano2zd	$⊢ J \in (0 ..^N) \to J + 1 \in ℤ$
35	34	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to J + 1 \in ℤ$
36	35	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to J + 1 \in ℤ$
37		fzossrbm1	$⊢ N \in ℤ \to (0 ..^N - 1) \subseteq (0 ..^N)$
38	2 37	syl	$⊢ J \in (0 ..^N) \to (0 ..^N - 1) \subseteq (0 ..^N)$
39	38	sseld	$⊢ J \in (0 ..^N) \to (y \in (0 ..^N - 1) \to y \in (0 ..^N))$
40	39	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (y \in (0 ..^N - 1) \to y \in (0 ..^N))$
41	40	imp	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y \in (0 ..^N)$
42		oveq2	$⊢ N = \|F\| \to (0 ..^N) = (0 ..^\|F\|)$
43	42	eleq2d	$⊢ N = \|F\| \to (y \in (0 ..^N) \leftrightarrow y \in (0 ..^\|F\|))$
44	43	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (y \in (0 ..^N) \leftrightarrow y \in (0 ..^\|F\|))$
45	44	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to (y \in (0 ..^N) \leftrightarrow y \in (0 ..^\|F\|))$
46	41 45	mpbid	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y \in (0 ..^\|F\|)$
47		cshwidxmod	$⊢ (F \in Word S \land J + 1 \in ℤ \land y \in (0 ..^\|F\|)) \to (F cyclShift (J + 1)) (y) = F ((y + J + 1) \mod \|F\|)$
48	33 36 46 47	syl3anc	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to (F cyclShift (J + 1)) (y) = F ((y + J + 1) \mod \|F\|)$
49	25	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to J \in ℤ$
50	49	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to J \in ℤ$
51		fzo0ss1	$⊢ (1 ..^N) \subseteq (0 ..^N)$
52	2	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to N \in ℤ$
53	52 3	sylan	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y + 1 \in (1 ..^N)$
54	51 53	sseldi	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y + 1 \in (0 ..^N)$
55	42	eleq2d	$⊢ N = \|F\| \to (y + 1 \in (0 ..^N) \leftrightarrow y + 1 \in (0 ..^\|F\|))$
56	55	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (y + 1 \in (0 ..^N) \leftrightarrow y + 1 \in (0 ..^\|F\|))$
57	56	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to (y + 1 \in (0 ..^N) \leftrightarrow y + 1 \in (0 ..^\|F\|))$
58	54 57	mpbid	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to y + 1 \in (0 ..^\|F\|)$
59		cshwidxmod	$⊢ (F \in Word S \land J \in ℤ \land y + 1 \in (0 ..^\|F\|)) \to (F cyclShift J) (y + 1) = F ((y + 1 + J) \mod \|F\|)$
60	33 50 58 59	syl3anc	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to (F cyclShift J) (y + 1) = F ((y + 1 + J) \mod \|F\|)$
61	32 48 60	3eqtr4rd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1)) \to (F cyclShift J) (y + 1) = (F cyclShift (J + 1)) (y)$
62	61	3adant3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1) \land x = y + 1) \to (F cyclShift J) (y + 1) = (F cyclShift (J + 1)) (y)$
63	21 62	eqtrd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1) \land x = y + 1) \to (F cyclShift J) (x) = (F cyclShift (J + 1)) (y)$
64	63	eqeq1d	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (0 ..^N - 1) \land x = y + 1) \to ((F cyclShift J) (x) = z \leftrightarrow (F cyclShift (J + 1)) (y) = z)$
65	7 19 64	rexxfrd2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (\exists x \in (1 ..^N) (F cyclShift J) (x) = z \leftrightarrow \exists y \in (0 ..^N - 1) (F cyclShift (J + 1)) (y) = z)$
66	65	abbidv	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to \{z \| \exists x \in (1 ..^N) (F cyclShift J) (x) = z\} = \{z \| \exists y \in (0 ..^N - 1) (F cyclShift (J + 1)) (y) = z\}$
67	25	anim2i	$⊢ (F \in Word S \land J \in (0 ..^N)) \to (F \in Word S \land J \in ℤ)$
68	67	3adant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F \in Word S \land J \in ℤ)$
69		cshwfn	$⊢ (F \in Word S \land J \in ℤ) \to (F cyclShift J) Fn (0 ..^\|F\|)$
70	68 69	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift J) Fn (0 ..^\|F\|)$
71		fnfun	$⊢ (F cyclShift J) Fn (0 ..^\|F\|) \to Fun (F cyclShift J)$
72	71	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift J) Fn (0 ..^\|F\|)) \to Fun (F cyclShift J)$
73	42	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (0 ..^N) = (0 ..^\|F\|)$
74	51 73	sseqtrid	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (1 ..^N) \subseteq (0 ..^\|F\|)$
75	74	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift J) Fn (0 ..^\|F\|)) \to (1 ..^N) \subseteq (0 ..^\|F\|)$
76		fndm	$⊢ (F cyclShift J) Fn (0 ..^\|F\|) \to dom (F cyclShift J) = (0 ..^\|F\|)$
77	76	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift J) Fn (0 ..^\|F\|)) \to dom (F cyclShift J) = (0 ..^\|F\|)$
78	75 77	sseqtrrd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift J) Fn (0 ..^\|F\|)) \to (1 ..^N) \subseteq dom (F cyclShift J)$
79	72 78	jca	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift J) Fn (0 ..^\|F\|)) \to (Fun (F cyclShift J) \land (1 ..^N) \subseteq dom (F cyclShift J))$
80	70 79	mpdan	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (Fun (F cyclShift J) \land (1 ..^N) \subseteq dom (F cyclShift J))$
81		dfimafn	$⊢ (Fun (F cyclShift J) \land (1 ..^N) \subseteq dom (F cyclShift J)) \to (F cyclShift J) [(1 ..^N)] = \{z \| \exists x \in (1 ..^N) (F cyclShift J) (x) = z\}$
82	80 81	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift J) [(1 ..^N)] = \{z \| \exists x \in (1 ..^N) (F cyclShift J) (x) = z\}$
83	34	anim2i	$⊢ (F \in Word S \land J \in (0 ..^N)) \to (F \in Word S \land J + 1 \in ℤ)$
84	83	3adant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F \in Word S \land J + 1 \in ℤ)$
85		cshwfn	$⊢ (F \in Word S \land J + 1 \in ℤ) \to (F cyclShift (J + 1)) Fn (0 ..^\|F\|)$
86	84 85	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift (J + 1)) Fn (0 ..^\|F\|)$
87		fnfun	$⊢ (F cyclShift (J + 1)) Fn (0 ..^\|F\|) \to Fun (F cyclShift (J + 1))$
88	87	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift (J + 1)) Fn (0 ..^\|F\|)) \to Fun (F cyclShift (J + 1))$
89	38	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (0 ..^N - 1) \subseteq (0 ..^N)$
90		oveq2	$⊢ \|F\| = N \to (0 ..^\|F\|) = (0 ..^N)$
91	90	eqcoms	$⊢ N = \|F\| \to (0 ..^\|F\|) = (0 ..^N)$
92	91	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (0 ..^\|F\|) = (0 ..^N)$
93	89 92	sseqtrrd	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (0 ..^N - 1) \subseteq (0 ..^\|F\|)$
94	93	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift (J + 1)) Fn (0 ..^\|F\|)) \to (0 ..^N - 1) \subseteq (0 ..^\|F\|)$
95		fndm	$⊢ (F cyclShift (J + 1)) Fn (0 ..^\|F\|) \to dom (F cyclShift (J + 1)) = (0 ..^\|F\|)$
96	95	adantl	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift (J + 1)) Fn (0 ..^\|F\|)) \to dom (F cyclShift (J + 1)) = (0 ..^\|F\|)$
97	94 96	sseqtrrd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift (J + 1)) Fn (0 ..^\|F\|)) \to (0 ..^N - 1) \subseteq dom (F cyclShift (J + 1))$
98	88 97	jca	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land (F cyclShift (J + 1)) Fn (0 ..^\|F\|)) \to (Fun (F cyclShift (J + 1)) \land (0 ..^N - 1) \subseteq dom (F cyclShift (J + 1)))$
99	86 98	mpdan	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (Fun (F cyclShift (J + 1)) \land (0 ..^N - 1) \subseteq dom (F cyclShift (J + 1)))$
100		dfimafn	$⊢ (Fun (F cyclShift (J + 1)) \land (0 ..^N - 1) \subseteq dom (F cyclShift (J + 1))) \to (F cyclShift (J + 1)) [(0 ..^N - 1)] = \{z \| \exists y \in (0 ..^N - 1) (F cyclShift (J + 1)) (y) = z\}$
101	99 100	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift (J + 1)) [(0 ..^N - 1)] = \{z \| \exists y \in (0 ..^N - 1) (F cyclShift (J + 1)) (y) = z\}$
102	66 82 101	3eqtr4d	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift J) [(1 ..^N)] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$
103	1 102	eqtrd	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift (J + 1)) [(0 ..^N - 1)]$

Metamath Proof Explorer

Theorem cshimadifsn0

Proof