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𝐺 ) ) )