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 ` CCfld ) |`s { 1 , -u 1 } )
Assertion	cnmsgn0g	|- 1 = ( 0g ` U )

Proof

Step	Hyp	Ref	Expression
1		cnmsgn0g.1	|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
2		cnring	|- CCfld e. Ring
3		eqid	|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
4	3	ringmgp	|- ( CCfld e. Ring -> ( mulGrp ` CCfld ) e. Mnd )
5	2 4	ax-mp	|- ( mulGrp ` CCfld ) e. Mnd
6		1ex	|- 1 e. _V
7	6	prid1	|- 1 e. { 1 , -u 1 }
8		ax-1cn	|- 1 e. CC
9		neg1cn	|- -u 1 e. CC
10		prssi	|- ( ( 1 e. CC /\ -u 1 e. CC ) -> { 1 , -u 1 } C_ CC )
11	8 9 10	mp2an	|- { 1 , -u 1 } C_ CC
12		cnfldbas	|- CC = ( Base ` CCfld )
13	3 12	mgpbas	|- CC = ( Base ` ( mulGrp ` CCfld ) )
14		cnfld1	|- 1 = ( 1r ` CCfld )
15	3 14	ringidval	|- 1 = ( 0g ` ( mulGrp ` CCfld ) )
16	1 13 15	ress0g	|- ( ( ( mulGrp ` CCfld ) e. Mnd /\ 1 e. { 1 , -u 1 } /\ { 1 , -u 1 } C_ CC ) -> 1 = ( 0g ` U ) )
17	5 7 11 16	mp3an	|- 1 = ( 0g ` U )