Metamath Proof Explorer


Theorem cnfldmul

Description: The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 27-Apr-2025)

Ref Expression
Assertion cnfldmul
|- x. = ( .r ` CCfld )

Proof

Step Hyp Ref Expression
1 ax-mulf
 |-  x. : ( CC X. CC ) --> CC
2 ffn
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
3 1 2 ax-mp
 |-  x. Fn ( CC X. CC )
4 fnov
 |-  ( x. Fn ( CC X. CC ) <-> x. = ( x e. CC , y e. CC |-> ( x x. y ) ) )
5 3 4 mpbi
 |-  x. = ( x e. CC , y e. CC |-> ( x x. y ) )
6 mpocnfldmul
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = ( .r ` CCfld )
7 5 6 eqtri
 |-  x. = ( .r ` CCfld )