i1fsub

Description: The difference of two simple functions is a simple function. (Contributed by Mario Carneiro, 6-Aug-2014)

		Ref	Expression
	Assertion	i1fsub	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F -_{f} G \in dom \int^{1}$

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
3		ax-resscn	$⊢ ℝ \subseteq ℂ$
4		fss	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to F : ℝ ⟶ ℂ$
5	2 3 4	sylancl	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℂ$
6		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
7		fss	$⊢ (G : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to G : ℝ ⟶ ℂ$
8	6 3 7	sylancl	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℂ$
9		ofnegsub	$⊢ (ℝ \in V \land F : ℝ ⟶ ℂ \land G : ℝ ⟶ ℂ) \to F +_{f} ((ℝ \times \{- 1\}) \times_{f} G) = F -_{f} G$
10	1 5 8 9	mp3an3an	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F +_{f} ((ℝ \times \{- 1\}) \times_{f} G) = F -_{f} G$
11		simpl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F \in dom \int^{1}$
12		simpr	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to G \in dom \int^{1}$
13		neg1rr	$⊢ - 1 \in ℝ$
14	13	a1i	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to - 1 \in ℝ$
15	12 14	i1fmulc	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to (ℝ \times \{- 1\}) \times_{f} G \in dom \int^{1}$
16	11 15	i1fadd	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F +_{f} ((ℝ \times \{- 1\}) \times_{f} G) \in dom \int^{1}$
17	10 16	eqeltrrd	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F -_{f} G \in dom \int^{1}$

Metamath Proof Explorer