Metamath Proof Explorer


Theorem cnmgpid

Description: The group identity element of nonzero complex number multiplication is one. (Contributed by Steve Rodriguez, 23-Feb-2007) (Revised by AV, 26-Aug-2021)

Ref Expression
Hypothesis cnmgpabl.m M=mulGrpfld𝑠0
Assertion cnmgpid 0M=1

Proof

Step Hyp Ref Expression
1 cnmgpabl.m M=mulGrpfld𝑠0
2 cnring fldRing
3 difss 0
4 ax-1cn 1
5 ax-1ne0 10
6 eldifsn 10110
7 4 5 6 mpbir2an 10
8 cnfldbas =Basefld
9 cnfld1 1=1fld
10 1 8 9 ringidss fldRing0101=0M
11 10 eqcomd fldRing0100M=1
12 2 3 7 11 mp3an 0M=1