Theorem fdivmptfv

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

	Ref	Expression
Assertion	fdivmptfv

Proof

Step	Hyp	Ref	Expression
1		fdivmpt
2	1	adantr
3		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
4		fveq2	$$⊢x=X\to G\left(x\right)=G\left(X\right)$$
5	3 4	oveq12d	$$⊢x=X\to \frac{F\left(x\right)}{G\left(x\right)}=\frac{F\left(X\right)}{G\left(X\right)}$$
6	5	adantl	$$⊢\left(\left(\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\wedge X\in {supp}_0\left(G\right)\right)\wedge x=X\right)\to \frac{F\left(x\right)}{G\left(x\right)}=\frac{F\left(X\right)}{G\left(X\right)}$$
7		simpr	$$⊢\left(\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\wedge X\in {supp}_0\left(G\right)\right)\to X\in {supp}_0\left(G\right)$$
8		ovexd	$$⊢\left(\left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)\wedge X\in {supp}_0\left(G\right)\right)\to \frac{F\left(X\right)}{G\left(X\right)}\in \mathrm{V}$$
9	2 6 7 8	fvmptd