Metamath Proof Explorer

Theorem refdivmptf

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

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> F : A --> RR )
2 suppssdm 
 |-  ( G supp 0 ) C_ dom G
3 fdm 
 |-  ( G : A --> RR -> dom G = A )
4 2 3 sseqtrid 
 |-  ( G : A --> RR -> ( G supp 0 ) C_ A )
5 4 3ad2ant2 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( G supp 0 ) C_ A )
6 5 sselda 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> x e. A )
7 1 6 ffvelrnd 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( F ` x ) e. RR )
8 simpl2 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> G : A --> RR )
9 8 6 ffvelrnd 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( G ` x ) e. RR )
10 ffn 
 |-  ( G : A --> RR -> G Fn A )
11 10 3ad2ant2 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> G Fn A )
12 simp3 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> A e. V )
13 0red 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> 0 e. RR )
14 elsuppfn 
 |-  ( ( G Fn A /\ A e. V /\ 0 e. RR ) -> ( x e. ( G supp 0 ) <-> ( x e. A /\ ( G ` x ) =/= 0 ) ) )
15 11 12 13 14 syl3anc 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( x e. ( G supp 0 ) <-> ( x e. A /\ ( G ` x ) =/= 0 ) ) )
16 15 simplbda 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( G ` x ) =/= 0 )
17 7 9 16 redivcld 
 |-  ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ x e. ( G supp 0 ) ) -> ( ( F ` x ) / ( G ` x ) ) e. RR )
18 17 fmpttd 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) : ( G supp 0 ) --> RR )
19 id 
 |-  ( F : A --> RR -> F : A --> RR )
20 ax-resscn 
 |-  RR C_ CC
21 20 a1i 
 |-  ( F : A --> RR -> RR C_ CC )
22 19 21 fssd 
 |-  ( F : A --> RR -> F : A --> CC )
23 id 
 |-  ( G : A --> RR -> G : A --> RR )
24 20 a1i 
 |-  ( G : A --> RR -> RR C_ CC )
25 23 24 fssd 
 |-  ( G : A --> RR -> G : A --> CC )
26 id 
 |-  ( A e. V -> A e. V )
27 22 25 26 3anim123i 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F : A --> CC /\ G : A --> CC /\ A e. V ) )
28 fdivmpt 
 |-  ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
29 27 28 syl 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
30 29 feq1d 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( ( F /_f G ) : ( G supp 0 ) --> RR <-> ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) : ( G supp 0 ) --> RR ) )
31 18 30 mpbird 
 |-  ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> RR )