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={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
Assertion	cnmsgnbas	$$⊢\left\{1,-1\right\}={\mathrm{Base}}_U$$

Proof

Step	Hyp	Ref	Expression
1		cnmsgngrp.u	$$⊢U={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
2		ax-1cn	$$⊢1\in ℂ$$
3		neg1cn	$$⊢-1\in ℂ$$
4		prssi	$$⊢\left(1\in ℂ\wedge -1\in ℂ\right)\to \left\{1,-1\right\}\subseteq ℂ$$
5	2 3 4	mp2an	$$⊢\left\{1,-1\right\}\subseteq ℂ$$
6		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
7		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
8	6 7	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
9	1 8	ressbas2	$$⊢\left\{1,-1\right\}\subseteq ℂ\to \left\{1,-1\right\}={\mathrm{Base}}_U$$
10	5 9	ax-mp	$$⊢\left\{1,-1\right\}={\mathrm{Base}}_U$$