This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )