Theorem cnsubrglem

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

	Ref	Expression
Hypotheses	cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
	cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
	cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
	cnsubrglem.4	⊢ 1 ∈ 𝐴
	cnsubrglem.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
Assertion	cnsubrglem	⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2		cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3		cnsubglem.3	⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
4		cnsubrglem.4	⊢ 1 ∈ 𝐴
5		cnsubrglem.5	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
6	1 2 3 4	cnsubglem	⊢ 𝐴 ∈ ( SubGrp ‘ ℂfld )
7	5	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴
8		cnring	⊢ ℂfld ∈ Ring
9		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
10		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
11		cnfldmul	⊢ · = ( .r ‘ ℂfld )
12	9 10 11	issubrg2	⊢ ( ℂfld ∈ Ring → ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) ) )
13	8 12	ax-mp	⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ↔ ( 𝐴 ∈ ( SubGrp ‘ ℂfld ) ∧ 1 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 · 𝑦 ) ∈ 𝐴 ) )
14	6 4 7 13	mpbir3an	⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )