Theorem i1fsub

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

	Ref	Expression
Assertion	i1fsub	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f − 𝐺 ) ∈ dom ∫1 )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
3		ax-resscn	⊢ ℝ ⊆ ℂ
4		fss	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
5	2 3 4	sylancl	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℂ )
6		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
7		fss	⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ℝ ⟶ ℂ )
8	6 3 7	sylancl	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℂ )
9		ofnegsub	⊢ ( ( ℝ ∈ V ∧ 𝐹 : ℝ ⟶ ℂ ∧ 𝐺 : ℝ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
10	1 5 8 9	mp3an3an	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
11		simpl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 ∈ dom ∫1 )
12		simpr	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 ∈ dom ∫1 )
13		neg1rr	⊢ - 1 ∈ ℝ
14	13	a1i	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → - 1 ∈ ℝ )
15	12 14	i1fmulc	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ∈ dom ∫1 )
16	11 15	i1fadd	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ∈ dom ∫1 )
17	10 16	eqeltrrd	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f − 𝐺 ) ∈ dom ∫1 )