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 ⊢ x ∈ A → x ∈ ℂ
cnsubglem.2 ⊢ x ∈ A ∧ y ∈ A → x + y ∈ A
cnsubmlem.3 ⊢ 0 ∈ A
Assertion cnsubmlem ⊢ A ∈ SubMnd ⁡ ℂ fld

Proof

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