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 
|- ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF - G ) ) = ( ( S.1 ` F ) - ( S.1 ` G ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> F e. dom S.1 )
2 simpr 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> G e. dom S.1 )
3 neg1rr 
 |-  -u 1 e. RR
4 3 a1i 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> -u 1 e. RR )
5 2 4 i1fmulc 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( ( RR X. { -u 1 } ) oF x. G ) e. dom S.1 )
6 1 5 itg1add 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) ) = ( ( S.1 ` F ) + ( S.1 ` ( ( RR X. { -u 1 } ) oF x. G ) ) ) )
7 2 4 itg1mulc 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( ( RR X. { -u 1 } ) oF x. G ) ) = ( -u 1 x. ( S.1 ` G ) ) )
8 itg1cl 
 |-  ( G e. dom S.1 -> ( S.1 ` G ) e. RR )
9 8 recnd 
 |-  ( G e. dom S.1 -> ( S.1 ` G ) e. CC )
10 2 9 syl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` G ) e. CC )
11 10 mulm1d 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( -u 1 x. ( S.1 ` G ) ) = -u ( S.1 ` G ) )
12 7 11 eqtrd 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( ( RR X. { -u 1 } ) oF x. G ) ) = -u ( S.1 ` G ) )
13 12 oveq2d 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( ( S.1 ` F ) + ( S.1 ` ( ( RR X. { -u 1 } ) oF x. G ) ) ) = ( ( S.1 ` F ) + -u ( S.1 ` G ) ) )
14 6 13 eqtrd 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) ) = ( ( S.1 ` F ) + -u ( S.1 ` G ) ) )
15 reex 
 |-  RR e. _V
16 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
17 ax-resscn 
 |-  RR C_ CC
18 fss 
 |-  ( ( F : RR --> RR /\ RR C_ CC ) -> F : RR --> CC )
19 16 17 18 sylancl 
 |-  ( F e. dom S.1 -> F : RR --> CC )
20 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
21 fss 
 |-  ( ( G : RR --> RR /\ RR C_ CC ) -> G : RR --> CC )
22 20 17 21 sylancl 
 |-  ( G e. dom S.1 -> G : RR --> CC )
23 ofnegsub 
 |-  ( ( RR e. _V /\ F : RR --> CC /\ G : RR --> CC ) -> ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
24 15 19 22 23 mp3an3an 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
25 24 fveq2d 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) ) = ( S.1 ` ( F oF - G ) ) )
26 itg1cl 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. RR )
27 26 recnd 
 |-  ( F e. dom S.1 -> ( S.1 ` F ) e. CC )
28 negsub 
 |-  ( ( ( S.1 ` F ) e. CC /\ ( S.1 ` G ) e. CC ) -> ( ( S.1 ` F ) + -u ( S.1 ` G ) ) = ( ( S.1 ` F ) - ( S.1 ` G ) ) )
29 27 9 28 syl2an 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( ( S.1 ` F ) + -u ( S.1 ` G ) ) = ( ( S.1 ` F ) - ( S.1 ` G ) ) )
30 14 25 29 3eqtr3d 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( S.1 ` ( F oF - G ) ) = ( ( S.1 ` F ) - ( S.1 ` G ) ) )