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

Proof

Step	Hyp	Ref	Expression
1		cnmsgn0g.1	$$⊢U={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
2		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
3		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
4	3	ringmgp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
5	2 4	ax-mp	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}$$
6		1ex	$$⊢1\in \mathrm{V}$$
7	6	prid1	$$⊢1\in \left\{1,-1\right\}$$
8		ax-1cn	$$⊢1\in ℂ$$
9		neg1cn	$$⊢-1\in ℂ$$
10		prssi	$$⊢\left(1\in ℂ\wedge -1\in ℂ\right)\to \left\{1,-1\right\}\subseteq ℂ$$
11	8 9 10	mp2an	$$⊢\left\{1,-1\right\}\subseteq ℂ$$
12		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
13	3 12	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
14		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
15	3 14	ringidval	$$⊢1=0_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
16	1 13 15	ress0g	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\in \mathrm{Mnd}\wedge 1\in \left\{1,-1\right\}\wedge \left\{1,-1\right\}\subseteq ℂ\right)\to 1=0_U$$
17	5 7 11 16	mp3an	$$⊢1=0_U$$