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	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
Assertion	cnmsgnbas	⊢ { 1 , - 1 } = ( Base ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnmsgngrp.u	⊢ 𝑈 = ( ( mulGrp ‘ ℂfld ) ↾s { 1 , - 1 } )
2		ax-1cn	⊢ 1 ∈ ℂ
3		neg1cn	⊢ - 1 ∈ ℂ
4		prssi	⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ) → { 1 , - 1 } ⊆ ℂ )
5	2 3 4	mp2an	⊢ { 1 , - 1 } ⊆ ℂ
6		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
7		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
8	6 7	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
9	1 8	ressbas2	⊢ ( { 1 , - 1 } ⊆ ℂ → { 1 , - 1 } = ( Base ‘ 𝑈 ) )
10	5 9	ax-mp	⊢ { 1 , - 1 } = ( Base ‘ 𝑈 )