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

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢F:A⟶ℝ\to F:A⟶ℝ$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3	2	a1i	$$⊢F:A⟶ℝ\to ℝ\subseteq ℂ$$
4	1 3	fssd	$$⊢F:A⟶ℝ\to F:A⟶ℂ$$
5		id	$$⊢G:A⟶ℝ\to G:A⟶ℝ$$
6	2	a1i	$$⊢G:A⟶ℝ\to ℝ\subseteq ℂ$$
7	5 6	fssd	$$⊢G:A⟶ℝ\to G:A⟶ℂ$$
8		id	$$⊢A\in V\to A\in V$$
9	4 7 8	3anim123i	$$⊢\left(F:A⟶ℝ\wedge G:A⟶ℝ\wedge A\in V\right)\to \left(F:A⟶ℂ\wedge G:A⟶ℂ\wedge A\in V\right)$$
10		fdivmpt
11	9 10	syl
12	11	adantr
13		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
14		fveq2	$$⊢x=X\to G\left(x\right)=G\left(X\right)$$
15	13 14	oveq12d	$$⊢x=X\to \frac{F\left(x\right)}{G\left(x\right)}=\frac{F\left(X\right)}{G\left(X\right)}$$
16	15	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)}$$
17		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)$$
18		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}$$
19	12 16 17 18	fvmptd