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	|- ( ( A e. CC /\ B e. CC ) -> ( A ( x e. CC , y e. CC |-> ( x x. y ) ) B ) = ( A x. B ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	|- ( ( x = A /\ y = B ) -> ( x x. y ) = ( A x. B ) )
2		eqid	|- ( x e. CC , y e. CC |-> ( x x. y ) ) = ( x e. CC , y e. CC |-> ( x x. y ) )
3		ovex	|- ( A x. B ) e. _V
4	1 2 3	ovmpoa	|- ( ( A e. CC /\ B e. CC ) -> ( A ( x e. CC , y e. CC |-> ( x x. y ) ) B ) = ( A x. B ) )