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

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
3 ax-resscn 
 |-  RR C_ CC
4 fss 
 |-  ( ( F : RR --> RR /\ RR C_ CC ) -> F : RR --> CC )
5 2 3 4 sylancl 
 |-  ( F e. dom S.1 -> F : RR --> CC )
6 i1ff 
 |-  ( G e. dom S.1 -> G : RR --> RR )
7 fss 
 |-  ( ( G : RR --> RR /\ RR C_ CC ) -> G : RR --> CC )
8 6 3 7 sylancl 
 |-  ( G e. dom S.1 -> G : RR --> CC )
9 ofnegsub 
 |-  ( ( RR e. _V /\ F : RR --> CC /\ G : RR --> CC ) -> ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
10 1 5 8 9 mp3an3an 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) = ( F oF - G ) )
11 simpl 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> F e. dom S.1 )
12 simpr 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> G e. dom S.1 )
13 neg1rr 
 |-  -u 1 e. RR
14 13 a1i 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> -u 1 e. RR )
15 12 14 i1fmulc 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( ( RR X. { -u 1 } ) oF x. G ) e. dom S.1 )
16 11 15 i1fadd 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oF + ( ( RR X. { -u 1 } ) oF x. G ) ) e. dom S.1 )
17 10 16 eqeltrrd 
 |-  ( ( F e. dom S.1 /\ G e. dom S.1 ) -> ( F oF - G ) e. dom S.1 )