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

Metamath Proof Explorer

Theorem itg1sub

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

Ref Expression
Assertion itg1sub ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 ∈ dom ∫1 )
2 simpr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 ∈ dom ∫1 )
3 neg1rr ⊢ - 1 ∈ ℝ
4 3 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → - 1 ∈ ℝ )
5 2 4 i1fmulc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ∈ dom ∫1 )
6 1 5 itg1add ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) )
7 2 4 itg1mulc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( - 1 · ( ∫1 ‘ 𝐺 ) ) )
8 itg1cl ⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
9 8 recnd ⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℂ )
10 2 9 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ 𝐺 ) ∈ ℂ )
11 10 mulm1d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( - 1 · ( ∫1 ‘ 𝐺 ) ) = - ( ∫1 ‘ 𝐺 ) )
12 7 11 eqtrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = - ( ∫1 ‘ 𝐺 ) )
13 12 oveq2d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) )
14 6 13 eqtrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) )
15 reex ⊢ ℝ ∈ V
16 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
17 ax-resscn ⊢ ℝ ⊆ ℂ
18 fss ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
19 16 17 18 sylancl ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℂ )
20 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
21 fss ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ℝ ⟶ ℂ )
22 20 17 21 sylancl ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℂ )
23 ofnegsub ⊢ ( ( ℝ ∈ V ∧ 𝐹 : ℝ ⟶ ℂ ∧ 𝐺 : ℝ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
24 15 19 22 23 mp3an3an ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
25 24 fveq2d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) )
26 itg1cl ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
27 26 recnd ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℂ )
28 negsub ⊢ ( ( ( ∫1 ‘ 𝐹 ) ∈ ℂ ∧ ( ∫1 ‘ 𝐺 ) ∈ ℂ ) → ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )
29 27 9 28 syl2an ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )
30 14 25 29 3eqtr3d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )