Metamath Proof Explorer


Theorem subcncff

Description: The subtraction of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses subcncff.f
|- ( ph -> F e. ( X -cn-> CC ) )
subcncff.g
|- ( ph -> G e. ( X -cn-> CC ) )
Assertion subcncff
|- ( ph -> ( F oF - G ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 subcncff.f
 |-  ( ph -> F e. ( X -cn-> CC ) )
2 subcncff.g
 |-  ( ph -> G e. ( X -cn-> CC ) )
3 cncfrss
 |-  ( F e. ( X -cn-> CC ) -> X C_ CC )
4 cnex
 |-  CC e. _V
5 4 ssex
 |-  ( X C_ CC -> X e. _V )
6 1 3 5 3syl
 |-  ( ph -> X e. _V )
7 cncff
 |-  ( F e. ( X -cn-> CC ) -> F : X --> CC )
8 1 7 syl
 |-  ( ph -> F : X --> CC )
9 8 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. CC )
10 cncff
 |-  ( G e. ( X -cn-> CC ) -> G : X --> CC )
11 2 10 syl
 |-  ( ph -> G : X --> CC )
12 11 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. CC )
13 8 feqmptd
 |-  ( ph -> F = ( x e. X |-> ( F ` x ) ) )
14 11 feqmptd
 |-  ( ph -> G = ( x e. X |-> ( G ` x ) ) )
15 6 9 12 13 14 offval2
 |-  ( ph -> ( F oF - G ) = ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) )
16 13 1 eqeltrrd
 |-  ( ph -> ( x e. X |-> ( F ` x ) ) e. ( X -cn-> CC ) )
17 14 2 eqeltrrd
 |-  ( ph -> ( x e. X |-> ( G ` x ) ) e. ( X -cn-> CC ) )
18 16 17 subcncf
 |-  ( ph -> ( x e. X |-> ( ( F ` x ) - ( G ` x ) ) ) e. ( X -cn-> CC ) )
19 15 18 eqeltrd
 |-  ( ph -> ( F oF - G ) e. ( X -cn-> CC ) )