Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	cnsubglem.1	$$⊢x\in A\to x\in ℂ$$
	cnsubglem.2	$$⊢\left(x\in A\wedge y\in A\right)\to x+y\in A$$
	cnsubglem.3	$$⊢x\in A\to -x\in A$$
	cnsubrglem.4	$$⊢1\in A$$
	cnsubrglem.5	$$⊢\left(x\in A\wedge y\in A\right)\to xy\in A$$
Assertion	cnsubrglem	$$⊢A\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnsubglem.1	$$⊢x\in A\to x\in ℂ$$
2		cnsubglem.2	$$⊢\left(x\in A\wedge y\in A\right)\to x+y\in A$$
3		cnsubglem.3	$$⊢x\in A\to -x\in A$$
4		cnsubrglem.4	$$⊢1\in A$$
5		cnsubrglem.5	$$⊢\left(x\in A\wedge y\in A\right)\to xy\in A$$
6	1 2 3 4	cnsubglem	$$⊢A\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
7	5	rgen2	$$⊢\forall x\in A\forall y\in Axy\in A$$
8		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
9		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
10		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
11		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
12	9 10 11	issubrg2	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to \left(A\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left(A\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge 1\in A\wedge \forall x\in A\forall y\in Axy\in A\right)\right)$$
13	8 12	ax-mp	$$⊢A\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left(A\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge 1\in A\wedge \forall x\in A\forall y\in Axy\in A\right)$$
14	6 4 7 13	mpbir3an	$$⊢A\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$