Metamath Proof Explorer


Theorem cnmsgn0g

Description: The neutral element of the sign subgroup of the complex numbers. (Contributed by Thierry Arnoux, 1-Nov-2023)

Ref Expression
Hypothesis cnmsgn0g.1 U = mulGrp fld 𝑠 1 1
Assertion cnmsgn0g 1 = 0 U

Proof

Step Hyp Ref Expression
1 cnmsgn0g.1 U = mulGrp fld 𝑠 1 1
2 cnring fld Ring
3 eqid mulGrp fld = mulGrp fld
4 3 ringmgp fld Ring mulGrp fld Mnd
5 2 4 ax-mp mulGrp fld Mnd
6 1ex 1 V
7 6 prid1 1 1 1
8 ax-1cn 1
9 neg1cn 1
10 prssi 1 1 1 1
11 8 9 10 mp2an 1 1
12 cnfldbas = Base fld
13 3 12 mgpbas = Base mulGrp fld
14 cnfld1 1 = 1 fld
15 3 14 ringidval 1 = 0 mulGrp fld
16 1 13 15 ress0g mulGrp fld Mnd 1 1 1 1 1 1 = 0 U
17 5 7 11 16 mp3an 1 = 0 U