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)

Ref Expression
Assertion cnfldmul ×=fld

Proof

Step Hyp Ref Expression
1 mulex ×V
2 cnfldstr fldStruct113
3 mulrid 𝑟=Slotndx
4 snsstp3 ndx×Basendx+ndx+ndx×
5 ssun1 Basendx+ndx+ndx×Basendx+ndx+ndx×*ndx*
6 ssun1 Basendx+ndx+ndx×*ndx*Basendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
7 df-cnfld fld=Basendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
8 6 7 sseqtrri Basendx+ndx+ndx×*ndx*fld
9 5 8 sstri Basendx+ndx+ndx×fld
10 4 9 sstri ndx×fld
11 2 3 10 strfv ×V×=fld
12 1 11 ax-mp ×=fld