ofnegsub

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

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

Proof

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

Metamath Proof Explorer

Theorem ofnegsub

Proof