Metamath Proof Explorer


Theorem fdivpm

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

Ref Expression
Assertion fdivpm F : A G : A A V F / f G 𝑝𝑚 A

Proof

Step Hyp Ref Expression
1 cnex V
2 1 a1i F : A G : A A V V
3 simp3 F : A G : A A V A V
4 fdivmptf F : A G : A A V F / f G : G supp 0
5 suppssdm G supp 0 dom G
6 fdm G : A dom G = A
7 6 eqcomd G : A A = dom G
8 7 3ad2ant2 F : A G : A A V A = dom G
9 5 8 sseqtrrid F : A G : A A V G supp 0 A
10 elpm2r V A V F / f G : G supp 0 G supp 0 A F / f G 𝑝𝑚 A
11 2 3 4 9 10 syl22anc F : A G : A A V F / f G 𝑝𝑚 A