This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )