Metamath Proof Explorer

Theorem fdivpm

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

Ref Expression
Assertion fdivpm 
|- ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) e. ( CC ^pm A ) )

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 1 a1i 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> CC e. _V )
3 simp3 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> A e. V )
4 fdivmptf 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> CC )
5 suppssdm 
 |-  ( G supp 0 ) C_ dom G
6 fdm 
 |-  ( G : A --> CC -> dom G = A )
7 6 eqcomd 
 |-  ( G : A --> CC -> A = dom G )
8 7 3ad2ant2 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> A = dom G )
9 5 8 sseqtrrid 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( G supp 0 ) C_ A )
10 elpm2r 
 |-  ( ( ( CC e. _V /\ A e. V ) /\ ( ( F /_f G ) : ( G supp 0 ) --> CC /\ ( G supp 0 ) C_ A ) ) -> ( F /_f G ) e. ( CC ^pm A ) )
11 2 3 4 9 10 syl22anc 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) e. ( CC ^pm A ) )