Metamath Proof Explorer

Theorem refdivpm

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

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

Proof

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