Theorem cnmsgnbas

Description: The base set of the sign subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypothesis	cnmsgngrp.u	|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
Assertion	cnmsgnbas	|- { 1 , -u 1 } = ( Base ` U )

Proof

Step	Hyp	Ref	Expression
1		cnmsgngrp.u	|- U = ( ( mulGrp ` CCfld ) |`s { 1 , -u 1 } )
2		ax-1cn	|- 1 e. CC
3		neg1cn	|- -u 1 e. CC
4		prssi	|- ( ( 1 e. CC /\ -u 1 e. CC ) -> { 1 , -u 1 } C_ CC )
5	2 3 4	mp2an	|- { 1 , -u 1 } C_ CC
6		eqid	|- ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
7		cnfldbas	|- CC = ( Base ` CCfld )
8	6 7	mgpbas	|- CC = ( Base ` ( mulGrp ` CCfld ) )
9	1 8	ressbas2	|- ( { 1 , -u 1 } C_ CC -> { 1 , -u 1 } = ( Base ` U ) )
10	5 9	ax-mp	|- { 1 , -u 1 } = ( Base ` U )