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