Theorem cnsubrglem

Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

	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	1	adantr	$$⊢\left(x\in A\wedge y\in A\right)\to x\in ℂ$$
8	1	ax-gen	$$⊢\forall x\left(x\in A\to x\in ℂ\right)$$
9		eleq1	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
10		eleq1	$$⊢x=y\to \left(x\in ℂ\leftrightarrow y\in ℂ\right)$$
11	9 10	imbi12d	$$⊢x=y\to \left(\left(x\in A\to x\in ℂ\right)\leftrightarrow \left(y\in A\to y\in ℂ\right)\right)$$
12	11	spvv	$$⊢\forall x\left(x\in A\to x\in ℂ\right)\to \left(y\in A\to y\in ℂ\right)$$
13	8 12	ax-mp	$$⊢y\in A\to y\in ℂ$$
14	13	adantl	$$⊢\left(x\in A\wedge y\in A\right)\to y\in ℂ$$
15	7 14	jca	$$⊢\left(x\in A\wedge y\in A\right)\to \left(x\in ℂ\wedge y\in ℂ\right)$$
16		ovmpot	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x\left(u\in ℂ,v\in ℂ⟼uv\right)y=xy$$
17	15 16	syl	$$⊢\left(x\in A\wedge y\in A\right)\to x\left(u\in ℂ,v\in ℂ⟼uv\right)y=xy$$
18	17	eqcomd	$$⊢\left(x\in A\wedge y\in A\right)\to xy=x\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
19	18	eleq1d	$$⊢\left(x\in A\wedge y\in A\right)\to \left(xy\in A\leftrightarrow x\left(u\in ℂ,v\in ℂ⟼uv\right)y\in A\right)$$
20	5 19	mpbid	$$⊢\left(x\in A\wedge y\in A\right)\to x\left(u\in ℂ,v\in ℂ⟼uv\right)y\in A$$
21	20	rgen2	$$⊢\forall x\in A\forall y\in Ax\left(u\in ℂ,v\in ℂ⟼uv\right)y\in A$$
22		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
23		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
24		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
25		mpocnfldmul	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
26	23 24 25	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 Ax\left(u\in ℂ,v\in ℂ⟼uv\right)y\in A\right)\right)$$
27	22 26	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 Ax\left(u\in ℂ,v\in ℂ⟼uv\right)y\in A\right)$$
28	6 4 21 27	mpbir3an	$$⊢A\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$