fargshiftf1

Description: If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017)

		Ref	Expression
	Hypothesis	fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
	Assertion	fargshiftf1	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} dom E$

Proof

Step	Hyp	Ref	Expression
1		fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
2		f1f	$⊢ F : (1 \dots N) \underset{1-1}{⟶} dom E \to F : (1 \dots N) ⟶ dom E$
3	1	fargshiftf	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to G : (0 ..^\|F\|) ⟶ dom E$
4	2 3	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to G : (0 ..^\|F\|) ⟶ dom E$
5		ffn	$⊢ F : (1 \dots N) ⟶ dom E \to F Fn (1 \dots N)$
6		fseq1hash	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$
7	5 6	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \|F\| = N$
8	2 7	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to \|F\| = N$
9		eleq1	$⊢ \|F\| = N \to (\|F\| \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
10		oveq2	$⊢ \|F\| = N \to (1 \dots \|F\|) = (1 \dots N)$
11		f1eq2	$⊢ (1 \dots \|F\|) = (1 \dots N) \to (F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E \leftrightarrow F : (1 \dots N) \underset{1-1}{⟶} dom E)$
12	10 11	syl	$⊢ \|F\| = N \to (F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E \leftrightarrow F : (1 \dots N) \underset{1-1}{⟶} dom E)$
13	9 12	anbi12d	$⊢ \|F\| = N \to ((\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E) \leftrightarrow (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E))$
14		dff13	$⊢ F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E \leftrightarrow (F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l))$
15		fz0add1fz1	$⊢ (\|F\| \in ℕ_{0} \land y \in (0 ..^\|F\|)) \to y + 1 \in (1 \dots \|F\|)$
16		fz0add1fz1	$⊢ (\|F\| \in ℕ_{0} \land z \in (0 ..^\|F\|)) \to z + 1 \in (1 \dots \|F\|)$
17	15 16	anim12dan	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))$
18		fveq2	$⊢ k = y + 1 \to F (k) = F (y + 1)$
19	18	eqeq1d	$⊢ k = y + 1 \to (F (k) = F (l) \leftrightarrow F (y + 1) = F (l))$
20		eqeq1	$⊢ k = y + 1 \to (k = l \leftrightarrow y + 1 = l)$
21	19 20	imbi12d	$⊢ k = y + 1 \to ((F (k) = F (l) \to k = l) \leftrightarrow (F (y + 1) = F (l) \to y + 1 = l))$
22		fveq2	$⊢ l = z + 1 \to F (l) = F (z + 1)$
23	22	eqeq2d	$⊢ l = z + 1 \to (F (y + 1) = F (l) \leftrightarrow F (y + 1) = F (z + 1))$
24		eqeq2	$⊢ l = z + 1 \to (y + 1 = l \leftrightarrow y + 1 = z + 1)$
25	23 24	imbi12d	$⊢ l = z + 1 \to ((F (y + 1) = F (l) \to y + 1 = l) \leftrightarrow (F (y + 1) = F (z + 1) \to y + 1 = z + 1))$
26	21 25	rspc2v	$⊢ (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|)) \to (\forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l) \to (F (y + 1) = F (z + 1) \to y + 1 = z + 1))$
27	26	adantl	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to (\forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l) \to (F (y + 1) = F (z + 1) \to y + 1 = z + 1))$
28	1	fargshiftfv	$⊢ (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E) \to (y \in (0 ..^\|F\|) \to G (y) = F (y + 1))$
29	28	expcom	$⊢ F : (1 \dots \|F\|) ⟶ dom E \to (\|F\| \in ℕ_{0} \to (y \in (0 ..^\|F\|) \to G (y) = F (y + 1)))$
30	29	com13	$⊢ y \in (0 ..^\|F\|) \to (\|F\| \in ℕ_{0} \to (F : (1 \dots \|F\|) ⟶ dom E \to G (y) = F (y + 1)))$
31	30	adantr	$⊢ (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to (\|F\| \in ℕ_{0} \to (F : (1 \dots \|F\|) ⟶ dom E \to G (y) = F (y + 1)))$
32	31	impcom	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (F : (1 \dots \|F\|) ⟶ dom E \to G (y) = F (y + 1))$
33	32	impcom	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \to G (y) = F (y + 1)$
34	1	fargshiftfv	$⊢ (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) ⟶ dom E) \to (z \in (0 ..^\|F\|) \to G (z) = F (z + 1))$
35	34	expcom	$⊢ F : (1 \dots \|F\|) ⟶ dom E \to (\|F\| \in ℕ_{0} \to (z \in (0 ..^\|F\|) \to G (z) = F (z + 1)))$
36	35	com13	$⊢ z \in (0 ..^\|F\|) \to (\|F\| \in ℕ_{0} \to (F : (1 \dots \|F\|) ⟶ dom E \to G (z) = F (z + 1)))$
37	36	adantl	$⊢ (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to (\|F\| \in ℕ_{0} \to (F : (1 \dots \|F\|) ⟶ dom E \to G (z) = F (z + 1)))$
38	37	impcom	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (F : (1 \dots \|F\|) ⟶ dom E \to G (z) = F (z + 1))$
39	38	impcom	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \to G (z) = F (z + 1)$
40	33 39	eqeq12d	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \to (G (y) = G (z) \leftrightarrow F (y + 1) = F (z + 1))$
41	40	adantr	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to (G (y) = G (z) \leftrightarrow F (y + 1) = F (z + 1))$
42	41	adantr	$⊢ (((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \land (F (y + 1) = F (z + 1) \to y + 1 = z + 1)) \to (G (y) = G (z) \leftrightarrow F (y + 1) = F (z + 1))$
43		elfzoelz	$⊢ y \in (0 ..^\|F\|) \to y \in ℤ$
44	43	zcnd	$⊢ y \in (0 ..^\|F\|) \to y \in ℂ$
45	44	adantr	$⊢ (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to y \in ℂ$
46	45	adantl	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to y \in ℂ$
47		elfzoelz	$⊢ z \in (0 ..^\|F\|) \to z \in ℤ$
48	47	zcnd	$⊢ z \in (0 ..^\|F\|) \to z \in ℂ$
49	48	adantl	$⊢ (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to z \in ℂ$
50	49	adantl	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to z \in ℂ$
51		1cnd	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to 1 \in ℂ$
52	46 50 51	3jca	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (y \in ℂ \land z \in ℂ \land 1 \in ℂ)$
53	52	adantl	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \to (y \in ℂ \land z \in ℂ \land 1 \in ℂ)$
54	53	adantr	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to (y \in ℂ \land z \in ℂ \land 1 \in ℂ)$
55		addcan2	$⊢ (y \in ℂ \land z \in ℂ \land 1 \in ℂ) \to (y + 1 = z + 1 \leftrightarrow y = z)$
56	54 55	syl	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to (y + 1 = z + 1 \leftrightarrow y = z)$
57	56	imbi2d	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to ((F (y + 1) = F (z + 1) \to y + 1 = z + 1) \leftrightarrow (F (y + 1) = F (z + 1) \to y = z))$
58	57	biimpa	$⊢ (((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \land (F (y + 1) = F (z + 1) \to y + 1 = z + 1)) \to (F (y + 1) = F (z + 1) \to y = z)$
59	42 58	sylbid	$⊢ (((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \land (F (y + 1) = F (z + 1) \to y + 1 = z + 1)) \to (G (y) = G (z) \to y = z)$
60	59	ex	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to ((F (y + 1) = F (z + 1) \to y + 1 = z + 1) \to (G (y) = G (z) \to y = z))$
61	27 60	syld	$⊢ ((F : (1 \dots \|F\|) ⟶ dom E \land (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)))) \land (y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|))) \to (\forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l) \to (G (y) = G (z) \to y = z))$
62	61	exp31	$⊢ F : (1 \dots \|F\|) ⟶ dom E \to ((\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to ((y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|)) \to (\forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l) \to (G (y) = G (z) \to y = z))))$
63	62	com24	$⊢ F : (1 \dots \|F\|) ⟶ dom E \to (\forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l) \to ((y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|)) \to ((\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (G (y) = G (z) \to y = z))))$
64	63	imp	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to ((y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|)) \to ((\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to (G (y) = G (z) \to y = z)))$
65	64	com13	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to ((y + 1 \in (1 \dots \|F\|) \land z + 1 \in (1 \dots \|F\|)) \to ((F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to (G (y) = G (z) \to y = z)))$
66	17 65	mpd	$⊢ (\|F\| \in ℕ_{0} \land (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|))) \to ((F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to (G (y) = G (z) \to y = z))$
67	66	expcom	$⊢ (y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to (\|F\| \in ℕ_{0} \to ((F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to (G (y) = G (z) \to y = z)))$
68	67	com13	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to (\|F\| \in ℕ_{0} \to ((y \in (0 ..^\|F\|) \land z \in (0 ..^\|F\|)) \to (G (y) = G (z) \to y = z)))$
69	68	ralrimdvv	$⊢ (F : (1 \dots \|F\|) ⟶ dom E \land \forall k \in (1 \dots \|F\|) \forall l \in (1 \dots \|F\|) (F (k) = F (l) \to k = l)) \to (\|F\| \in ℕ_{0} \to \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z))$
70	14 69	sylbi	$⊢ F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E \to (\|F\| \in ℕ_{0} \to \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z))$
71	70	impcom	$⊢ (\|F\| \in ℕ_{0} \land F : (1 \dots \|F\|) \underset{1-1}{⟶} dom E) \to \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z)$
72	13 71	syl6bir	$⊢ \|F\| = N \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z))$
73	8 72	mpcom	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z)$
74		dff13	$⊢ G : (0 ..^\|F\|) \underset{1-1}{⟶} dom E \leftrightarrow (G : (0 ..^\|F\|) ⟶ dom E \land \forall y \in (0 ..^\|F\|) \forall z \in (0 ..^\|F\|) (G (y) = G (z) \to y = z))$
75	4 73 74	sylanbrc	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{1-1}{⟶} dom E) \to G : (0 ..^\|F\|) \underset{1-1}{⟶} dom E$

Metamath Proof Explorer

Theorem fargshiftf1

Proof