Metamath Proof Explorer

Theorem fdivmpt

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

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

Proof

Step Hyp Ref Expression
1 fex 
 |-  ( ( F : A --> CC /\ A e. V ) -> F e. _V )
2 1 3adant2 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> F e. _V )
3 fex 
 |-  ( ( G : A --> CC /\ A e. V ) -> G e. _V )
4 3 3adant1 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> G e. _V )
5 fdivval 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F /_f G ) = ( ( F oF / G ) |` ( G supp 0 ) ) )
6 offres 
 |-  ( ( F e. _V /\ G e. _V ) -> ( ( F oF / G ) |` ( G supp 0 ) ) = ( ( F |` ( G supp 0 ) ) oF / ( G |` ( G supp 0 ) ) ) )
7 5 6 eqtrd 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F /_f G ) = ( ( F |` ( G supp 0 ) ) oF / ( G |` ( G supp 0 ) ) ) )
8 2 4 7 syl2anc 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( ( F |` ( G supp 0 ) ) oF / ( G |` ( G supp 0 ) ) ) )
9 ffn 
 |-  ( F : A --> CC -> F Fn A )
10 9 3ad2ant1 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> F Fn A )
11 suppssdm 
 |-  ( G supp 0 ) C_ dom G
12 fdm 
 |-  ( G : A --> CC -> dom G = A )
13 12 eqcomd 
 |-  ( G : A --> CC -> A = dom G )
14 13 3ad2ant2 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> A = dom G )
15 11 14 sseqtrrid 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( G supp 0 ) C_ A )
16 fnssres 
 |-  ( ( F Fn A /\ ( G supp 0 ) C_ A ) -> ( F |` ( G supp 0 ) ) Fn ( G supp 0 ) )
17 10 15 16 syl2anc 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F |` ( G supp 0 ) ) Fn ( G supp 0 ) )
18 ffn 
 |-  ( G : A --> CC -> G Fn A )
19 18 3ad2ant2 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> G Fn A )
20 fnssres 
 |-  ( ( G Fn A /\ ( G supp 0 ) C_ A ) -> ( G |` ( G supp 0 ) ) Fn ( G supp 0 ) )
21 19 15 20 syl2anc 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( G |` ( G supp 0 ) ) Fn ( G supp 0 ) )
22 ovexd 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( G supp 0 ) e. _V )
23 inidm 
 |-  ( ( G supp 0 ) i^i ( G supp 0 ) ) = ( G supp 0 )
24 fvres 
 |-  ( x e. ( G supp 0 ) -> ( ( F |` ( G supp 0 ) ) ` x ) = ( F ` x ) )
25 24 adantl 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( ( F |` ( G supp 0 ) ) ` x ) = ( F ` x ) )
26 fvres 
 |-  ( x e. ( G supp 0 ) -> ( ( G |` ( G supp 0 ) ) ` x ) = ( G ` x ) )
27 26 adantl 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( ( G |` ( G supp 0 ) ) ` x ) = ( G ` x ) )
28 17 21 22 22 23 25 27 offval 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( ( F |` ( G supp 0 ) ) oF / ( G |` ( G supp 0 ) ) ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
29 8 28 eqtrd 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )