cshimadifsn

Description: The image of a cyclically shifted word under its domain without its left 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	cshimadifsn	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift J) [(1 ..^N)]$

Proof

Step	Hyp	Ref	Expression
1		wrdfn	$⊢ F \in Word S \to F Fn (0 ..^\|F\|)$
2		fnfun	$⊢ F Fn (0 ..^\|F\|) \to Fun F$
3	1 2	syl	$⊢ F \in Word S \to Fun F$
4	3	3ad2ant1	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to Fun F$
5		wrddm	$⊢ F \in Word S \to dom F = (0 ..^\|F\|)$
6		difssd	$⊢ (dom F = (0 ..^\|F\|) \land N = \|F\|) \to (0 ..^\|F\|) ∖ \{J\} \subseteq (0 ..^\|F\|)$
7		oveq2	$⊢ N = \|F\| \to (0 ..^N) = (0 ..^\|F\|)$
8	7	difeq1d	$⊢ N = \|F\| \to (0 ..^N) ∖ \{J\} = (0 ..^\|F\|) ∖ \{J\}$
9	8	adantl	$⊢ (dom F = (0 ..^\|F\|) \land N = \|F\|) \to (0 ..^N) ∖ \{J\} = (0 ..^\|F\|) ∖ \{J\}$
10		simpl	$⊢ (dom F = (0 ..^\|F\|) \land N = \|F\|) \to dom F = (0 ..^\|F\|)$
11	6 9 10	3sstr4d	$⊢ (dom F = (0 ..^\|F\|) \land N = \|F\|) \to (0 ..^N) ∖ \{J\} \subseteq dom F$
12	11	a1d	$⊢ (dom F = (0 ..^\|F\|) \land N = \|F\|) \to (J \in (0 ..^N) \to (0 ..^N) ∖ \{J\} \subseteq dom F)$
13	12	ex	$⊢ dom F = (0 ..^\|F\|) \to (N = \|F\| \to (J \in (0 ..^N) \to (0 ..^N) ∖ \{J\} \subseteq dom F))$
14	5 13	syl	$⊢ F \in Word S \to (N = \|F\| \to (J \in (0 ..^N) \to (0 ..^N) ∖ \{J\} \subseteq dom F))$
15	14	3imp	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (0 ..^N) ∖ \{J\} \subseteq dom F$
16	4 15	jca	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (Fun F \land (0 ..^N) ∖ \{J\} \subseteq dom F)$
17		dfimafn	$⊢ (Fun F \land (0 ..^N) ∖ \{J\} \subseteq dom F) \to F [(0 ..^N) ∖ \{J\}] = \{z \| \exists x \in ((0 ..^N) ∖ \{J\}) F (x) = z\}$
18	16 17	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = \{z \| \exists x \in ((0 ..^N) ∖ \{J\}) F (x) = z\}$
19		modsumfzodifsn	$⊢ (J \in (0 ..^N) \land y \in (1 ..^N)) \to (y + J) \mod N \in ((0 ..^N) ∖ \{J\})$
20	19	3ad2antl3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to (y + J) \mod N \in ((0 ..^N) ∖ \{J\})$
21		oveq2	$⊢ \|F\| = N \to (y + J) \mod \|F\| = (y + J) \mod N$
22	21	eqcoms	$⊢ N = \|F\| \to (y + J) \mod \|F\| = (y + J) \mod N$
23	22	eleq1d	$⊢ N = \|F\| \to ((y + J) \mod \|F\| \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (y + J) \mod N \in ((0 ..^N) ∖ \{J\}))$
24	23	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to ((y + J) \mod \|F\| \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (y + J) \mod N \in ((0 ..^N) ∖ \{J\}))$
25	24	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to ((y + J) \mod \|F\| \in ((0 ..^N) ∖ \{J\}) \leftrightarrow (y + J) \mod N \in ((0 ..^N) ∖ \{J\}))$
26	20 25	mpbird	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to (y + J) \mod \|F\| \in ((0 ..^N) ∖ \{J\})$
27		modfzo0difsn	$⊢ (J \in (0 ..^N) \land x \in ((0 ..^N) ∖ \{J\})) \to \exists y \in (1 ..^N) x = (y + J) \mod N$
28	27	3ad2antl3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in ((0 ..^N) ∖ \{J\})) \to \exists y \in (1 ..^N) x = (y + J) \mod N$
29		oveq2	$⊢ N = \|F\| \to (y + J) \mod N = (y + J) \mod \|F\|$
30	29	eqcomd	$⊢ N = \|F\| \to (y + J) \mod \|F\| = (y + J) \mod N$
31	30	eqeq2d	$⊢ N = \|F\| \to (x = (y + J) \mod \|F\| \leftrightarrow x = (y + J) \mod N)$
32	31	rexbidv	$⊢ N = \|F\| \to (\exists y \in (1 ..^N) x = (y + J) \mod \|F\| \leftrightarrow \exists y \in (1 ..^N) x = (y + J) \mod N)$
33	32	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (\exists y \in (1 ..^N) x = (y + J) \mod \|F\| \leftrightarrow \exists y \in (1 ..^N) x = (y + J) \mod N)$
34	33	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in ((0 ..^N) ∖ \{J\})) \to (\exists y \in (1 ..^N) x = (y + J) \mod \|F\| \leftrightarrow \exists y \in (1 ..^N) x = (y + J) \mod N)$
35	28 34	mpbird	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land x \in ((0 ..^N) ∖ \{J\})) \to \exists y \in (1 ..^N) x = (y + J) \mod \|F\|$
36		fveq2	$⊢ x = (y + J) \mod \|F\| \to F (x) = F ((y + J) \mod \|F\|)$
37	36	3ad2ant3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N) \land x = (y + J) \mod \|F\|) \to F (x) = F ((y + J) \mod \|F\|)$
38		simpl1	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to F \in Word S$
39		elfzoelz	$⊢ J \in (0 ..^N) \to J \in ℤ$
40	39	3ad2ant3	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to J \in ℤ$
41	40	adantr	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to J \in ℤ$
42		oveq2	$⊢ N = \|F\| \to (1 ..^N) = (1 ..^\|F\|)$
43	42	eleq2d	$⊢ N = \|F\| \to (y \in (1 ..^N) \leftrightarrow y \in (1 ..^\|F\|))$
44		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
45	44	sseli	$⊢ y \in (1 ..^\|F\|) \to y \in (0 ..^\|F\|)$
46	43 45	biimtrdi	$⊢ N = \|F\| \to (y \in (1 ..^N) \to y \in (0 ..^\|F\|))$
47	46	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (y \in (1 ..^N) \to y \in (0 ..^\|F\|))$
48	47	imp	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to y \in (0 ..^\|F\|)$
49		cshwidxmod	$⊢ (F \in Word S \land J \in ℤ \land y \in (0 ..^\|F\|)) \to (F cyclShift J) (y) = F ((y + J) \mod \|F\|)$
50	49	eqcomd	$⊢ (F \in Word S \land J \in ℤ \land y \in (0 ..^\|F\|)) \to F ((y + J) \mod \|F\|) = (F cyclShift J) (y)$
51	38 41 48 50	syl3anc	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N)) \to F ((y + J) \mod \|F\|) = (F cyclShift J) (y)$
52	51	3adant3	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N) \land x = (y + J) \mod \|F\|) \to F ((y + J) \mod \|F\|) = (F cyclShift J) (y)$
53	37 52	eqtrd	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N) \land x = (y + J) \mod \|F\|) \to F (x) = (F cyclShift J) (y)$
54	53	eqeq1d	$⊢ ((F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \land y \in (1 ..^N) \land x = (y + J) \mod \|F\|) \to (F (x) = z \leftrightarrow (F cyclShift J) (y) = z)$
55	26 35 54	rexxfrd2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (\exists x \in ((0 ..^N) ∖ \{J\}) F (x) = z \leftrightarrow \exists y \in (1 ..^N) (F cyclShift J) (y) = z)$
56	55	abbidv	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to \{z \| \exists x \in ((0 ..^N) ∖ \{J\}) F (x) = z\} = \{z \| \exists y \in (1 ..^N) (F cyclShift J) (y) = z\}$
57	39	anim2i	$⊢ (F \in Word S \land J \in (0 ..^N)) \to (F \in Word S \land J \in ℤ)$
58	57	3adant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F \in Word S \land J \in ℤ)$
59		cshwfn	$⊢ (F \in Word S \land J \in ℤ) \to (F cyclShift J) Fn (0 ..^\|F\|)$
60	58 59	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift J) Fn (0 ..^\|F\|)$
61		fnfun	$⊢ (F cyclShift J) Fn (0 ..^\|F\|) \to Fun (F cyclShift J)$
62	61	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)$
63	42 44	eqsstrdi	$⊢ N = \|F\| \to (1 ..^N) \subseteq (0 ..^\|F\|)$
64	63	3ad2ant2	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (1 ..^N) \subseteq (0 ..^\|F\|)$
65	64	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\|)$
66		fndm	$⊢ (F cyclShift J) Fn (0 ..^\|F\|) \to dom (F cyclShift J) = (0 ..^\|F\|)$
67	66	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\|)$
68	65 67	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)$
69	62 68	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))$
70	60 69	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))$
71		dfimafn	$⊢ (Fun (F cyclShift J) \land (1 ..^N) \subseteq dom (F cyclShift J)) \to (F cyclShift J) [(1 ..^N)] = \{z \| \exists y \in (1 ..^N) (F cyclShift J) (y) = z\}$
72	70 71	syl	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to (F cyclShift J) [(1 ..^N)] = \{z \| \exists y \in (1 ..^N) (F cyclShift J) (y) = z\}$
73	56 72	eqtr4d	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to \{z \| \exists x \in ((0 ..^N) ∖ \{J\}) F (x) = z\} = (F cyclShift J) [(1 ..^N)]$
74	18 73	eqtrd	$⊢ (F \in Word S \land N = \|F\| \land J \in (0 ..^N)) \to F [(0 ..^N) ∖ \{J\}] = (F cyclShift J) [(1 ..^N)]$

Metamath Proof Explorer

Theorem cshimadifsn

Proof