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 G : A A V X supp 0 G F / f G X = F X G X

Proof

Step Hyp Ref Expression
1 id F : A F : A
2 ax-resscn
3 2 a1i F : A
4 1 3 fssd F : A F : A
5 id G : A G : A
6 2 a1i G : A
7 5 6 fssd G : A G : A
8 id A V A V
9 4 7 8 3anim123i F : A G : A A V F : A G : A A V
10 fdivmpt F : A G : A A V F / f G = x supp 0 G F x G x
11 9 10 syl F : A G : A A V F / f G = x supp 0 G F x G x
12 11 adantr F : A G : A A V X supp 0 G F / f G = x supp 0 G 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 G : A A V X supp 0 G x = X F x G x = F X G X
17 simpr F : A G : A A V X supp 0 G X supp 0 G
18 ovexd F : A G : A A V X supp 0 G F X G X V
19 12 16 17 18 fvmptd F : A G : A A V X supp 0 G F / f G X = F X G X