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	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 /f 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℝ )
2		ax-resscn	⊢ ℝ ⊆ ℂ
3	2	a1i	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ℝ ⊆ ℂ )
4	1 3	fssd	⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℂ )
5		id	⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐺 : 𝐴 ⟶ ℝ )
6	2	a1i	⊢ ( 𝐺 : 𝐴 ⟶ ℝ → ℝ ⊆ ℂ )
7	5 6	fssd	⊢ ( 𝐺 : 𝐴 ⟶ ℝ → 𝐺 : 𝐴 ⟶ ℂ )
8		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
9	4 7 8	3anim123i	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) )
10		fdivmpt	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
11	9 10	syl	⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
12	11	adantr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
13		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
14		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
15	13 14	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )
16	15	adantl	⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )
17		simpr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → 𝑋 ∈ ( 𝐺 supp 0 ) )
18		ovexd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ V )
19	12 16 17 18	fvmptd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐺 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 /f 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )