Theorem ovmul

Description: Multiplication of complex numbers produces the same value as multiplication expressed in maps-to notation of the same complex numbers. (Contributed by GG, 16-Mar-2025)

	Ref	Expression
Assertion	ovmul	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝐵 ) = ( 𝐴 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 · 𝑦 ) = ( 𝐴 · 𝐵 ) )
2		eqid	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) )
3		ovex	⊢ ( 𝐴 · 𝐵 ) ∈ V
4	1 2 3	ovmpoa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) 𝐵 ) = ( 𝐴 · 𝐵 ) )