fargshiftfva

Description: The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017)

		Ref	Expression
	Hypothesis	fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
	Assertion	fargshiftfva	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to \forall l \in (0 ..^N) E (G (l)) = ⦋ (l + 1) / x ⦌ P)$

Proof

Step	Hyp	Ref	Expression
1		fargshift.g	$⊢ G = (x \in (0 ..^\|F\|) ⟼ F (x + 1))$
2		fz0add1fz1	$⊢ (N \in ℕ_{0} \land l \in (0 ..^N)) \to l + 1 \in (1 \dots N)$
3		simpl	$⊢ (l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \to l + 1 \in (1 \dots N)$
4	3	adantr	$⊢ ((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \to l + 1 \in (1 \dots N)$
5		2fveq3	$⊢ k = l + 1 \to E (F (k)) = E (F (l + 1))$
6		csbeq1	$⊢ k = l + 1 \to ⦋ k / x ⦌ P = ⦋ (l + 1) / x ⦌ P$
7	5 6	eqeq12d	$⊢ k = l + 1 \to (E (F (k)) = ⦋ k / x ⦌ P \leftrightarrow E (F (l + 1)) = ⦋ (l + 1) / x ⦌ P)$
8	7	adantl	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to (E (F (k)) = ⦋ k / x ⦌ P \leftrightarrow E (F (l + 1)) = ⦋ (l + 1) / x ⦌ P)$
9		simpl	$⊢ (N \in ℕ_{0} \land l \in (0 ..^N)) \to N \in ℕ_{0}$
10	9	adantl	$⊢ (l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \to N \in ℕ_{0}$
11	10	anim1i	$⊢ ((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \to (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E)$
12	11	adantr	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E)$
13		simpr	$⊢ (N \in ℕ_{0} \land l \in (0 ..^N)) \to l \in (0 ..^N)$
14	13	ad3antlr	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to l \in (0 ..^N)$
15	1	fargshiftfv	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (l \in (0 ..^N) \to G (l) = F (l + 1))$
16	15	imp	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land l \in (0 ..^N)) \to G (l) = F (l + 1)$
17	16	eqcomd	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land l \in (0 ..^N)) \to F (l + 1) = G (l)$
18	12 14 17	syl2anc	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to F (l + 1) = G (l)$
19	18	fveqeq2d	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to (E (F (l + 1)) = ⦋ (l + 1) / x ⦌ P \leftrightarrow E (G (l)) = ⦋ (l + 1) / x ⦌ P)$
20	8 19	bitrd	$⊢ (((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \land k = l + 1) \to (E (F (k)) = ⦋ k / x ⦌ P \leftrightarrow E (G (l)) = ⦋ (l + 1) / x ⦌ P)$
21	4 20	rspcdv	$⊢ ((l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \land F : (1 \dots N) ⟶ dom E) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to E (G (l)) = ⦋ (l + 1) / x ⦌ P)$
22	21	ex	$⊢ (l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \to (F : (1 \dots N) ⟶ dom E \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to E (G (l)) = ⦋ (l + 1) / x ⦌ P))$
23	22	com23	$⊢ (l + 1 \in (1 \dots N) \land (N \in ℕ_{0} \land l \in (0 ..^N))) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to (F : (1 \dots N) ⟶ dom E \to E (G (l)) = ⦋ (l + 1) / x ⦌ P))$
24	2 23	mpancom	$⊢ (N \in ℕ_{0} \land l \in (0 ..^N)) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to (F : (1 \dots N) ⟶ dom E \to E (G (l)) = ⦋ (l + 1) / x ⦌ P))$
25	24	ex	$⊢ N \in ℕ_{0} \to (l \in (0 ..^N) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to (F : (1 \dots N) ⟶ dom E \to E (G (l)) = ⦋ (l + 1) / x ⦌ P)))$
26	25	com24	$⊢ N \in ℕ_{0} \to (F : (1 \dots N) ⟶ dom E \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to (l \in (0 ..^N) \to E (G (l)) = ⦋ (l + 1) / x ⦌ P)))$
27	26	imp31	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land \forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P) \to (l \in (0 ..^N) \to E (G (l)) = ⦋ (l + 1) / x ⦌ P)$
28	27	ralrimiv	$⊢ ((N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \land \forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P) \to \forall l \in (0 ..^N) E (G (l)) = ⦋ (l + 1) / x ⦌ P$
29	28	ex	$⊢ (N \in ℕ_{0} \land F : (1 \dots N) ⟶ dom E) \to (\forall k \in (1 \dots N) E (F (k)) = ⦋ k / x ⦌ P \to \forall l \in (0 ..^N) E (G (l)) = ⦋ (l + 1) / x ⦌ P)$

Metamath Proof Explorer

Theorem fargshiftfva

Proof