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

Proof

Step	Hyp	Ref	Expression
1		fdivmpt	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
2	1	adantr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( 𝐹 /f 𝐺 ) = ( 𝑥 ∈ ( 𝐺 supp 0 ) ↦ ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) ) )
3		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
4		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑋 ) )
5	3 4	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )
6	5	adantl	⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )
7		simpr	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → 𝑋 ∈ ( 𝐺 supp 0 ) )
8		ovexd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) ∈ V )
9	2 6 7 8	fvmptd	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑋 ∈ ( 𝐺 supp 0 ) ) → ( ( 𝐹 /f 𝐺 ) ‘ 𝑋 ) = ( ( 𝐹 ‘ 𝑋 ) / ( 𝐺 ‘ 𝑋 ) ) )