itg1sub

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F \in dom \int^{1}$
2		simpr	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to G \in dom \int^{1}$
3		neg1rr	$⊢ - 1 \in ℝ$
4	3	a1i	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to - 1 \in ℝ$
5	2 4	i1fmulc	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to (ℝ \times \{- 1\}) \times_{f} G \in dom \int^{1}$
6	1 5	itg1add	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F +_{f} ((ℝ \times \{- 1\}) \times_{f} G)) = \int^{1} (F) + \int^{1} ((ℝ \times \{- 1\}) \times_{f} G)$
7	2 4	itg1mulc	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} ((ℝ \times \{- 1\}) \times_{f} G) = -1 \int^{1} (G)$
8		itg1cl	$⊢ G \in dom \int^{1} \to \int^{1} (G) \in ℝ$
9	8	recnd	$⊢ G \in dom \int^{1} \to \int^{1} (G) \in ℂ$
10	2 9	syl	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (G) \in ℂ$
11	10	mulm1d	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to -1 \int^{1} (G) = - \int^{1} (G)$
12	7 11	eqtrd	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} ((ℝ \times \{- 1\}) \times_{f} G) = - \int^{1} (G)$
13	12	oveq2d	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F) + \int^{1} ((ℝ \times \{- 1\}) \times_{f} G) = \int^{1} (F) + (- \int^{1} (G))$
14	6 13	eqtrd	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F +_{f} ((ℝ \times \{- 1\}) \times_{f} G)) = \int^{1} (F) + (- \int^{1} (G))$
15		reex	$⊢ ℝ \in V$
16		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
17		ax-resscn	$⊢ ℝ \subseteq ℂ$
18		fss	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to F : ℝ ⟶ ℂ$
19	16 17 18	sylancl	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℂ$
20		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
21		fss	$⊢ (G : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to G : ℝ ⟶ ℂ$
22	20 17 21	sylancl	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℂ$
23		ofnegsub	$⊢ (ℝ \in V \land F : ℝ ⟶ ℂ \land G : ℝ ⟶ ℂ) \to F +_{f} ((ℝ \times \{- 1\}) \times_{f} G) = F -_{f} G$
24	15 19 22 23	mp3an3an	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to F +_{f} ((ℝ \times \{- 1\}) \times_{f} G) = F -_{f} G$
25	24	fveq2d	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F +_{f} ((ℝ \times \{- 1\}) \times_{f} G)) = \int^{1} (F -_{f} G)$
26		itg1cl	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℝ$
27	26	recnd	$⊢ F \in dom \int^{1} \to \int^{1} (F) \in ℂ$
28		negsub	$⊢ (\int^{1} (F) \in ℂ \land \int^{1} (G) \in ℂ) \to \int^{1} (F) + (- \int^{1} (G)) = \int^{1} (F) - \int^{1} (G)$
29	27 9 28	syl2an	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F) + (- \int^{1} (G)) = \int^{1} (F) - \int^{1} (G)$
30	14 25 29	3eqtr3d	$⊢ (F \in dom \int^{1} \land G \in dom \int^{1}) \to \int^{1} (F -_{f} G) = \int^{1} (F) - \int^{1} (G)$

Metamath Proof Explorer

Theorem itg1sub

Proof