Theorem cnsubmlem

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

	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$$
	cnsubmlem.3	$$⊢0\in A$$
Assertion	cnsubmlem	$$⊢A\in \mathrm{SubMnd}\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		cnsubmlem.3	$$⊢0\in A$$
4	1	ssriv	$$⊢A\subseteq ℂ$$
5	2	rgen2	$$⊢\forall x\in A\forall y\in Ax+y\in A$$
6		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
7		ringmnd	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
8		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
9		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
10		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
11	8 9 10	issubm	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\to \left(A\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left(A\subseteq ℂ\wedge 0\in A\wedge \forall x\in A\forall y\in Ax+y\in A\right)\right)$$
12	6 7 11	mp2b	$$⊢A\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\leftrightarrow \left(A\subseteq ℂ\wedge 0\in A\wedge \forall x\in A\forall y\in Ax+y\in A\right)$$
13	4 3 5 12	mpbir3an	$$⊢A\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$