Theorem cnsubmlem

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

	Ref	Expression
Hypotheses	cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
	cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
	cnsubmlem.3	⊢ 0 ∈ 𝐴
Assertion	cnsubmlem	⊢ 𝐴 ∈ ( SubMnd ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cnsubglem.1	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2		cnsubglem.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3		cnsubmlem.3	⊢ 0 ∈ 𝐴
4	1	ssriv	⊢ 𝐴 ⊆ ℂ
5	2	rgen2	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴
6		cnring	⊢ ℂfld ∈ Ring
7		ringmnd	⊢ ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
8		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
9		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
10		cnfldadd	⊢ + = ( +g ‘ ℂfld )
11	8 9 10	issubm	⊢ ( ℂfld ∈ Mnd → ( 𝐴 ∈ ( SubMnd ‘ ℂfld ) ↔ ( 𝐴 ⊆ ℂ ∧ 0 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ) ) )
12	6 7 11	mp2b	⊢ ( 𝐴 ∈ ( SubMnd ‘ ℂfld ) ↔ ( 𝐴 ⊆ ℂ ∧ 0 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 + 𝑦 ) ∈ 𝐴 ) )
13	4 3 5 12	mpbir3an	⊢ 𝐴 ∈ ( SubMnd ‘ ℂfld )