Metamath Proof Explorer


Theorem fdivmptf

Description: The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020)

Ref Expression
Assertion fdivmptf
|- ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> CC )

Proof

Step Hyp Ref Expression
1 simpl1
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> F : A --> CC )
2 suppssdm
 |-  ( G supp 0 ) C_ dom G
3 fdm
 |-  ( G : A --> CC -> dom G = A )
4 2 3 sseqtrid
 |-  ( G : A --> CC -> ( G supp 0 ) C_ A )
5 4 3ad2ant2
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( G supp 0 ) C_ A )
6 5 sselda
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> x e. A )
7 1 6 ffvelrnd
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( F ` x ) e. CC )
8 simpl2
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> G : A --> CC )
9 8 6 ffvelrnd
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( G ` x ) e. CC )
10 ffn
 |-  ( G : A --> CC -> G Fn A )
11 10 3ad2ant2
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> G Fn A )
12 simp3
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> A e. V )
13 0cnd
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> 0 e. CC )
14 elsuppfn
 |-  ( ( G Fn A /\ A e. V /\ 0 e. CC ) -> ( x e. ( G supp 0 ) <-> ( x e. A /\ ( G ` x ) =/= 0 ) ) )
15 11 12 13 14 syl3anc
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( x e. ( G supp 0 ) <-> ( x e. A /\ ( G ` x ) =/= 0 ) ) )
16 15 simplbda
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( G ` x ) =/= 0 )
17 7 9 16 divcld
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( ( F ` x ) / ( G ` x ) ) e. CC )
18 17 fmpttd
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) : ( G supp 0 ) --> CC )
19 fdivmpt
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
20 19 feq1d
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( ( F /_f G ) : ( G supp 0 ) --> CC <-> ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) : ( G supp 0 ) --> CC ) )
21 18 20 mpbird
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> CC )