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 )