Metamath Proof Explorer

Theorem fdivmptfv

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

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

Proof

Step Hyp Ref Expression
1 fdivmpt 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
2 1 adantr 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
3 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
4 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
5 3 4 oveq12d 
 |-  ( x = X -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` X ) / ( G ` X ) ) )
6 5 adantl 
 |-  ( ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) /\ x = X ) -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` X ) / ( G ` X ) ) )
7 simpr 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) -> X e. ( G supp 0 ) )
8 ovexd 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F ` X ) / ( G ` X ) ) e. _V )
9 2 6 7 8 fvmptd 
 |-  ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F /_f G ) ` X ) = ( ( F ` X ) / ( G ` X ) ) )