fargshiftfo

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

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

Proof

Step	Hyp	Ref	Expression
1		fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
2		fof	$⊢ F : (1 \dots N) \underset{onto}{⟶} 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{onto}{⟶} dom E) \to G : (0 ..^\|F\|) ⟶ dom E$
5	1	rnmpt	$⊢ ran G = \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\}$
6		fofn	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to F Fn (1 \dots N)$
7		fnrnfv	$⊢ F Fn (1 \dots N) \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
8	6 7	syl	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
9	8	adantl	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\}$
10		df-fo	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \leftrightarrow (F Fn (1 \dots N) \land ran F = dom E)$
11	10	biimpi	$⊢ F : (1 \dots N) \underset{onto}{⟶} dom E \to (F Fn (1 \dots N) \land ran F = dom E)$
12	11	adantl	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (F Fn (1 \dots N) \land ran F = dom E)$
13		eqeq1	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow dom E = \{y \| \exists z \in (1 \dots N) y = F (z)\})$
14		eqcom	$⊢ dom E = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E$
15	13 14	bitrdi	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \leftrightarrow \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E)$
16		ffn	$⊢ F : (1 \dots N) ⟶ dom E \to F Fn (1 \dots N)$
17		fseq1hash	$⊢ (N \in ℕ_{0} \land F Fn (1 \dots N)) \to \|F\| = N$
18	16 17	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to \|F\| = N$
19	2 18	sylan2	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \|F\| = N$
20		fz0add1fz1	$⊢ (N \in ℕ_{0} \land x \in (0 ..^N)) \to x + 1 \in (1 \dots N)$
21		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
22		fzval3	$⊢ N \in ℤ \to (1 \dots N) = (1 ..^N + 1)$
23	21 22	syl	$⊢ N \in ℕ_{0} \to (1 \dots N) = (1 ..^N + 1)$
24		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
25		1cnd	$⊢ N \in ℕ_{0} \to 1 \in ℂ$
26	24 25	addcomd	$⊢ N \in ℕ_{0} \to N + 1 = 1 + N$
27	26	oveq2d	$⊢ N \in ℕ_{0} \to (1 ..^N + 1) = (1 ..^1 + N)$
28	23 27	eqtrd	$⊢ N \in ℕ_{0} \to (1 \dots N) = (1 ..^1 + N)$
29	28	eleq2d	$⊢ N \in ℕ_{0} \to (z \in (1 \dots N) \leftrightarrow z \in (1 ..^1 + N))$
30	29	biimpa	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z \in (1 ..^1 + N)$
31	21	adantr	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to N \in ℤ$
32		fzosubel3	$⊢ (z \in (1 ..^1 + N) \land N \in ℤ) \to z - 1 \in (0 ..^N)$
33	30 31 32	syl2anc	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z - 1 \in (0 ..^N)$
34		oveq1	$⊢ x = z - 1 \to x + 1 = z - 1 + 1$
35	34	eqeq2d	$⊢ x = z - 1 \to (z = x + 1 \leftrightarrow z = z - 1 + 1)$
36	35	adantl	$⊢ ((N \in ℕ_{0} \land z \in (1 \dots N)) \land x = z - 1) \to (z = x + 1 \leftrightarrow z = z - 1 + 1)$
37		elfzelz	$⊢ z \in (1 \dots N) \to z \in ℤ$
38	37	zcnd	$⊢ z \in (1 \dots N) \to z \in ℂ$
39	38	adantl	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z \in ℂ$
40		1cnd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to 1 \in ℂ$
41	39 40	npcand	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z - 1 + 1 = z$
42	41	eqcomd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to z = z - 1 + 1$
43	33 36 42	rspcedvd	$⊢ (N \in ℕ_{0} \land z \in (1 \dots N)) \to \exists x \in (0 ..^N) z = x + 1$
44		fveq2	$⊢ z = x + 1 \to F (z) = F (x + 1)$
45	44	eqeq2d	$⊢ z = x + 1 \to (y = F (z) \leftrightarrow y = F (x + 1))$
46	45	adantl	$⊢ (N \in ℕ_{0} \land z = x + 1) \to (y = F (z) \leftrightarrow y = F (x + 1))$
47	20 43 46	rexxfrd	$⊢ N \in ℕ_{0} \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
48	47	adantr	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
49		oveq2	$⊢ \|F\| = N \to (0 ..^\|F\|) = (0 ..^N)$
50	49	rexeqdv	$⊢ \|F\| = N \to (\exists x \in (0 ..^\|F\|) y = F (x + 1) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1))$
51	50	bibi2d	$⊢ \|F\| = N \to ((\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1)) \leftrightarrow (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1)))$
52	51	adantl	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to ((\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1)) \leftrightarrow (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^N) y = F (x + 1)))$
53	48 52	mpbird	$⊢ (N \in ℕ_{0} \land \|F\| = N) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1))$
54	19 53	syldan	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (\exists z \in (1 \dots N) y = F (z) \leftrightarrow \exists x \in (0 ..^\|F\|) y = F (x + 1))$
55	54	abbidv	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists z \in (1 \dots N) y = F (z)\} = \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\}$
56	55	eqeq1d	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (\{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E \leftrightarrow \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
57	56	biimpcd	$⊢ \{y \| \exists z \in (1 \dots N) y = F (z)\} = dom E \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
58	15 57	syl6bi	$⊢ ran F = dom E \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
59	58	com23	$⊢ ran F = dom E \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
60	59	adantl	$⊢ (F Fn (1 \dots N) \land ran F = dom E) \to ((N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E))$
61	12 60	mpcom	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to (ran F = \{y \| \exists z \in (1 \dots N) y = F (z)\} \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E)$
62	9 61	mpd	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to \{y \| \exists x \in (0 ..^\|F\|) y = F (x + 1)\} = dom E$
63	5 62	eqtrid	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to ran G = dom E$
64		dffo2	$⊢ G : (0 ..^\|F\|) \underset{onto}{⟶} dom E \leftrightarrow (G : (0 ..^\|F\|) ⟶ dom E \land ran G = dom E)$
65	4 63 64	sylanbrc	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) \underset{onto}{⟶} dom E) \to G : (0 ..^\|F\|) \underset{onto}{⟶} dom E$

Metamath Proof Explorer

Theorem fargshiftfo

Proof