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