shftfn

Description: Functionality and domain of a sequence shifted by A . (Contributed by NM, 20-Jul-2005) (Revised by Mario Carneiro, 3-Nov-2013)

		Ref	Expression
	Hypothesis	shftfval.1	$⊢ F \in V$
	Assertion	shftfn	$⊢ (F Fn B \land A \in ℂ) \to (F shift A) Fn \{x \in ℂ \| x - A \in B\}$

Proof

Step	Hyp	Ref	Expression
1		shftfval.1	$⊢ F \in V$
2		relopabv	$⊢ Rel \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
3	2	a1i	$⊢ (F Fn B \land A \in ℂ) \to Rel \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
4		fnfun	$⊢ F Fn B \to Fun F$
5	4	adantr	$⊢ (F Fn B \land A \in ℂ) \to Fun F$
6		funmo	$⊢ Fun F \to \exists^{*} w (z - A) F w$
7		vex	$⊢ z \in V$
8		vex	$⊢ w \in V$
9		eleq1w	$⊢ x = z \to (x \in ℂ \leftrightarrow z \in ℂ)$
10		oveq1	$⊢ x = z \to x - A = z - A$
11	10	breq1d	$⊢ x = z \to ((x - A) F y \leftrightarrow (z - A) F y)$
12	9 11	anbi12d	$⊢ x = z \to ((x \in ℂ \land (x - A) F y) \leftrightarrow (z \in ℂ \land (z - A) F y))$
13		breq2	$⊢ y = w \to ((z - A) F y \leftrightarrow (z - A) F w)$
14	13	anbi2d	$⊢ y = w \to ((z \in ℂ \land (z - A) F y) \leftrightarrow (z \in ℂ \land (z - A) F w))$
15		eqid	$⊢ \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} = \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
16	7 8 12 14 15	brab	$⊢ z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w \leftrightarrow (z \in ℂ \land (z - A) F w)$
17	16	simprbi	$⊢ z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w \to (z - A) F w$
18	17	moimi	$⊢ \exists^{} w (z - A) F w \to \exists^{} w z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w$
19	6 18	syl	$⊢ Fun F \to \exists^{*} w z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w$
20	19	alrimiv	$⊢ Fun F \to \forall z \exists^{*} w z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w$
21	5 20	syl	$⊢ (F Fn B \land A \in ℂ) \to \forall z \exists^{*} w z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w$
22		dffun6	$⊢ Fun \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} \leftrightarrow (Rel \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} \land \forall z \exists^{*} w z \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\} w)$
23	3 21 22	sylanbrc	$⊢ (F Fn B \land A \in ℂ) \to Fun \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
24	1	shftfval	$⊢ A \in ℂ \to F shift A = \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
25	24	adantl	$⊢ (F Fn B \land A \in ℂ) \to F shift A = \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\}$
26	25	funeqd	$⊢ (F Fn B \land A \in ℂ) \to (Fun (F shift A) \leftrightarrow Fun \{⟨x, y⟩ \| (x \in ℂ \land (x - A) F y)\})$
27	23 26	mpbird	$⊢ (F Fn B \land A \in ℂ) \to Fun (F shift A)$
28	1	shftdm	$⊢ A \in ℂ \to dom (F shift A) = \{x \in ℂ \| x - A \in dom F\}$
29		fndm	$⊢ F Fn B \to dom F = B$
30	29	eleq2d	$⊢ F Fn B \to (x - A \in dom F \leftrightarrow x - A \in B)$
31	30	rabbidv	$⊢ F Fn B \to \{x \in ℂ \| x - A \in dom F\} = \{x \in ℂ \| x - A \in B\}$
32	28 31	sylan9eqr	$⊢ (F Fn B \land A \in ℂ) \to dom (F shift A) = \{x \in ℂ \| x - A \in B\}$
33		df-fn	$⊢ (F shift A) Fn \{x \in ℂ \| x - A \in B\} \leftrightarrow (Fun (F shift A) \land dom (F shift A) = \{x \in ℂ \| x - A \in B\})$
34	27 32 33	sylanbrc	$⊢ (F Fn B \land A \in ℂ) \to (F shift A) Fn \{x \in ℂ \| x - A \in B\}$

Metamath Proof Explorer

Theorem shftfn

Proof