Metamath Proof Explorer


Theorem cnfld0

Description: Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion cnfld0 0=0fld

Proof

Step Hyp Ref Expression
1 00id 0+0=0
2 cnring fldRing
3 ringgrp fldRingfldGrp
4 2 3 ax-mp fldGrp
5 0cn 0
6 cnfldbas =Basefld
7 cnfldadd +=+fld
8 eqid 0fld=0fld
9 6 7 8 grpid fldGrp00+0=00fld=0
10 4 5 9 mp2an 0+0=00fld=0
11 1 10 mpbi 0fld=0
12 11 eqcomi 0=0fld