Theorem ofnegsub

Description: Function analogue of negsub . (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Assertion	ofnegsub	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to F{+}_f\left(\left(A\times \left\{-1\right\}\right){\times }_{f}G\right)=F{-}_{f}G$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to A\in V$$
2		simp2	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to F:A⟶ℂ$$
3	2	ffnd	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to FFnA$$
4		ax-1cn	$$⊢1\in ℂ$$
5	4	negcli	$$⊢-1\in ℂ$$
6		fnconstg	$$⊢-1\in ℂ\to \left(A\times \left\{-1\right\}\right)FnA$$
7	5 6	mp1i	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to \left(A\times \left\{-1\right\}\right)FnA$$
8		simp3	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to G:A⟶ℂ$$
9	8	ffnd	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to GFnA$$
10		inidm	$$⊢A\cap A=A$$
11	7 9 1 1 10	offn	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to \left(\left(A\times \left\{-1\right\}\right){\times }_{f}G\right)FnA$$
12	3 9 1 1 10	offn	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to \left(F{-}_{f}G\right)FnA$$
13		eqidd	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)=F\left(x\right)$$
14	5	a1i	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to -1\in ℂ$$
15		eqidd	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to G\left(x\right)=G\left(x\right)$$
16	1 14 9 15	ofc1	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to \left(\left(A\times \left\{-1\right\}\right){\times }_{f}G\right)\left(x\right)=-1G\left(x\right)$$
17	8	ffvelcdmda	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to G\left(x\right)\in ℂ$$
18	17	mulm1d	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to -1G\left(x\right)=-G\left(x\right)$$
19	16 18	eqtrd	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to \left(\left(A\times \left\{-1\right\}\right){\times }_{f}G\right)\left(x\right)=-G\left(x\right)$$
20	2	ffvelcdmda	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)\in ℂ$$
21	20 17	negsubd	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)+\left(-G\left(x\right)\right)=F\left(x\right)-G\left(x\right)$$
22	3 9 1 1 10 13 15	ofval	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to \left(F{-}_{f}G\right)\left(x\right)=F\left(x\right)-G\left(x\right)$$
23	21 22	eqtr4d	$$⊢\left(\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\wedge x\in A\right)\to F\left(x\right)+\left(-G\left(x\right)\right)=\left(F{-}_{f}G\right)\left(x\right)$$
24	1 3 11 12 13 19 23	offveq	$$⊢\left(A\in V\wedge F:A⟶ℂ\wedge G:A⟶ℂ\right)\to F{+}_f\left(\left(A\times \left\{-1\right\}\right){\times }_{f}G\right)=F{-}_{f}G$$