Theorem cnmsubglem

Description: Lemma for rpmsubg and friends. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Hypotheses	cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
	cnmsubglem.1	$$⊢x\in A\to x\in ℂ$$
	cnmsubglem.2	$$⊢x\in A\to x\ne 0$$
	cnmsubglem.3	$$⊢\left(x\in A\wedge y\in A\right)\to xy\in A$$
	cnmsubglem.4	$$⊢1\in A$$
	cnmsubglem.5	$$⊢x\in A\to \frac{1}{x}\in A$$
Assertion	cnmsubglem	$$⊢A\in \mathrm{SubGrp}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnmgpabl.m	$$⊢M={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}{\upharpoonright }_{𝑠}\left(ℂ\setminus \left\{0\right\}\right)$$
2		cnmsubglem.1	$$⊢x\in A\to x\in ℂ$$
3		cnmsubglem.2	$$⊢x\in A\to x\ne 0$$
4		cnmsubglem.3	$$⊢\left(x\in A\wedge y\in A\right)\to xy\in A$$
5		cnmsubglem.4	$$⊢1\in A$$
6		cnmsubglem.5	$$⊢x\in A\to \frac{1}{x}\in A$$
7		eldifsn	$$⊢x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(x\in ℂ\wedge x\ne 0\right)$$
8	2 3 7	sylanbrc	$$⊢x\in A\to x\in \left(ℂ\setminus \left\{0\right\}\right)$$
9	8	ssriv	$$⊢A\subseteq ℂ\setminus \left\{0\right\}$$
10	5	ne0ii	$$⊢A\ne \varnothing$$
11	4	ralrimiva	$$⊢x\in A\to \forall y\in Axy\in A$$
12		cnfldinv	$$⊢\left(x\in ℂ\wedge x\ne 0\right)\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)=\frac{1}{x}$$
13	2 3 12	syl2anc	$$⊢x\in A\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)=\frac{1}{x}$$
14	13 6	eqeltrd	$$⊢x\in A\to {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)\in A$$
15	11 14	jca	$$⊢x\in A\to \left(\forall y\in Axy\in A\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)\in A\right)$$
16	15	rgen	$$⊢\forall x\in A\left(\forall y\in Axy\in A\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)\in A\right)$$
17	1	cnmgpabl	$$⊢M\in \mathrm{Abel}$$
18		ablgrp	$$⊢M\in \mathrm{Abel}\to M\in \mathrm{Grp}$$
19		difss	$$⊢ℂ\setminus \left\{0\right\}\subseteq ℂ$$
20		eqid	$$⊢{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$$
21		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
22	20 21	mgpbas	$$⊢ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
23	1 22	ressbas2	$$⊢ℂ\setminus \left\{0\right\}\subseteq ℂ\to ℂ\setminus \left\{0\right\}={\mathrm{Base}}_M$$
24	19 23	ax-mp	$$⊢ℂ\setminus \left\{0\right\}={\mathrm{Base}}_M$$
25		cnex	$$⊢ℂ\in \mathrm{V}$$
26		difexg	$$⊢ℂ\in \mathrm{V}\to ℂ\setminus \left\{0\right\}\in \mathrm{V}$$
27		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
28	20 27	mgpplusg	$$⊢\times ={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
29	1 28	ressplusg	$$⊢ℂ\setminus \left\{0\right\}\in \mathrm{V}\to \times ={+}_M$$
30	25 26 29	mp2b	$$⊢\times ={+}_M$$
31		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
32		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
33	21 31 32	drngui	$$⊢ℂ\setminus \left\{0\right\}=\mathrm{Unit}\left({ℂ}_{\mathrm{fld}}\right)$$
34		eqid	$$⊢{inv}_r\left({ℂ}_{\mathrm{fld}}\right)={inv}_r\left({ℂ}_{\mathrm{fld}}\right)$$
35	33 1 34	invrfval	$$⊢{inv}_r\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left(M\right)$$
36	24 30 35	issubg2	$$⊢M\in \mathrm{Grp}\to \left(A\in \mathrm{SubGrp}\left(M\right)\leftrightarrow \left(A\subseteq ℂ\setminus \left\{0\right\}\wedge A\ne \varnothing \wedge \forall x\in A\left(\forall y\in Axy\in A\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)\in A\right)\right)\right)$$
37	17 18 36	mp2b	$$⊢A\in \mathrm{SubGrp}\left(M\right)\leftrightarrow \left(A\subseteq ℂ\setminus \left\{0\right\}\wedge A\ne \varnothing \wedge \forall x\in A\left(\forall y\in Axy\in A\wedge {inv}_r\left({ℂ}_{\mathrm{fld}}\right)\left(x\right)\in A\right)\right)$$
38	9 10 16 37	mpbir3an	$$⊢A\in \mathrm{SubGrp}\left(M\right)$$