Theorem cnmsgngrp

Description: The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypothesis	cnmsgngrp.u	$$⊢U={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
Assertion	cnmsgngrp	$$⊢U\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		cnmsgngrp.u	$$⊢U={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
2		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
3	2	cnmsgnsubg	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)$$
4		cnex	$$⊢ℂ\in \mathrm{V}$$
5	4	difexi	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{V}$$
6		ax-1cn	$$⊢1\in ℂ$$
7		ax-1ne0	$$⊢1\ne 0$$
8		eldifsn	$$⊢1\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(1\in ℂ\wedge 1\ne 0\right)$$
9	6 7 8	mpbir2an	$$⊢1\in \left(ℂ\setminus \left\{0\right\}\right)$$
10		neg1cn	$$⊢-1\in ℂ$$
11		neg1ne0	$$⊢-1\ne 0$$
12		eldifsn	$$⊢-1\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(-1\in ℂ\wedge -1\ne 0\right)$$
13	10 11 12	mpbir2an	$$⊢-1\in \left(ℂ\setminus \left\{0\right\}\right)$$
14		prssi	$$⊢\left(1\in \left(ℂ\setminus \left\{0\right\}\right)\wedge -1\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to \left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}$$
15	9 13 14	mp2an	$$⊢\left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}$$
16		ressabs	$$⊢\left(ℂ\setminus \left\{0\right\}\in \mathrm{V}\wedge \left\{1,-1\right\}\subseteq ℂ\setminus \left\{0\right\}\right)\to \left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
17	5 15 16	mp2an	$$⊢\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
18	1 17	eqtr4i	$$⊢U=\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right){\upharpoonright }_{𝑠}\left\{1,-1\right\}$$
19	18	subggrp	$$⊢\left\{1,-1\right\}\in \mathrm{SubGrp}\left({\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)\right)\to U\in \mathrm{Grp}$$
20	3 19	ax-mp	$$⊢U\in \mathrm{Grp}$$