Theorem ofsubid

Description: Function analogue of subid . (Contributed by Steve Rodriguez, 5-Nov-2015)

	Ref	Expression
Assertion	ofsubid	$$⊢\left(A\in V\wedge F:A⟶ℂ\right)\to F{-}_{f}F=A\times \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in V\wedge F:A⟶ℂ\right)\to A\in V$$
2		ffn	$$⊢F:A⟶ℂ\to FFnA$$
3	2	adantl	$$⊢\left(A\in V\wedge F:A⟶ℂ\right)\to FFnA$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	fconst	$$⊢\left(A\times \left\{0\right\}\right):A⟶\left\{0\right\}$$
6		ffn	$$⊢\left(A\times \left\{0\right\}\right):A⟶\left\{0\right\}\to \left(A\times \left\{0\right\}\right)FnA$$
7	5 6	mp1i	$$⊢\left(A\in V\wedge F:A⟶ℂ\right)\to \left(A\times \left\{0\right\}\right)FnA$$
8		eqidd	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
9		ffvelrn	$$⊢\left(F:A⟶ℂ\wedge x\in A\right)\to F\left(x\right)\in ℂ$$
10	9	subidd	$$⊢\left(F:A⟶ℂ\wedge x\in A\right)\to F\left(x\right)-F\left(x\right)=0$$
11	10	adantll	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)-F\left(x\right)=0$$
12	4	fvconst2	$$⊢x\in A\to \left(A\times \left\{0\right\}\right)\left(x\right)=0$$
13	12	adantl	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\right)\wedge x\in A\right)\to \left(A\times \left\{0\right\}\right)\left(x\right)=0$$
14	11 13	eqtr4d	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)-F\left(x\right)=\left(A\times \left\{0\right\}\right)\left(x\right)$$
15	1 3 3 7 8 8 14	offveq	$$⊢\left(A\in V\wedge F:A⟶ℂ\right)\to F{-}_{f}F=A\times \left\{0\right\}$$