Metamath Proof Explorer

Theorem refdivmptfv

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( F : A --> RR -> F : A --> RR )
2 ax-resscn 
 |-  RR C_ CC
3 2 a1i 
 |-  ( F : A --> RR -> RR C_ CC )
4 1 3 fssd 
 |-  ( F : A --> RR -> F : A --> CC )
5 id 
 |-  ( G : A --> RR -> G : A --> RR )
6 2 a1i 
 |-  ( G : A --> RR -> RR C_ CC )
7 5 6 fssd 
 |-  ( G : A --> RR -> G : A --> CC )
8 id 
 |-  ( A e. V -> A e. V )
9 4 7 8 3anim123i 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F : A --> CC /\ G : A --> CC /\ A e. V ) )
10 fdivmpt 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
11 9 10 syl 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
12 11 adantr 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
13 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
14 fveq2 
 |-  ( x = X -> ( G ` x ) = ( G ` X ) )
15 13 14 oveq12d 
 |-  ( x = X -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` X ) / ( G ` X ) ) )
16 15 adantl 
 |-  ( ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) /\ x = X ) -> ( ( F ` x ) / ( G ` x ) ) = ( ( F ` X ) / ( G ` X ) ) )
17 simpr 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) -> X e. ( G supp 0 ) )
18 ovexd 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F ` X ) / ( G ` X ) ) e. _V )
19 12 16 17 18 fvmptd 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F /_f G ) ` X ) = ( ( F ` X ) / ( G ` X ) ) )