Metamath Proof Explorer

Theorem cnsubrglemOLD

Description: Obsolete version of cnsubrglem as of 30-Apr-2025. (Contributed by Mario Carneiro, 4-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cnsubglem.1 ⊢ x ∈ A → x ∈ ℂ
cnsubglem.2 ⊢ x ∈ A ∧ y ∈ A → x + y ∈ A
cnsubglem.3 ⊢ x ∈ A → − x ∈ A
cnsubrglem.4 ⊢ 1 ∈ A
cnsubrglem.5 ⊢ x ∈ A ∧ y ∈ A → x ⁢ y ∈ A
Assertion cnsubrglemOLD ⊢ A ∈ SubRing ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 cnsubglem.1 ⊢ x ∈ A → x ∈ ℂ
2 cnsubglem.2 ⊢ x ∈ A ∧ y ∈ A → x + y ∈ A
3 cnsubglem.3 ⊢ x ∈ A → − x ∈ A
4 cnsubrglem.4 ⊢ 1 ∈ A
5 cnsubrglem.5 ⊢ x ∈ A ∧ y ∈ A → x ⁢ y ∈ A
6 1 2 3 4 cnsubglem ⊢ A ∈ SubGrp ⁡ ℂ fld
7 5 rgen2 ⊢ ∀ x ∈ A ∀ y ∈ A x ⁢ y ∈ A
8 cnring ⊢ ℂ fld ∈ Ring
9 cnfldbas ⊢ ℂ = Base ℂ fld
10 cnfld1 ⊢ 1 = 1 ℂ fld
11 cnfldmul ⊢ × = ⋅ ℂ fld
12 9 10 11 issubrg2 ⊢ ℂ fld ∈ Ring → A ∈ SubRing ⁡ ℂ fld ↔ A ∈ SubGrp ⁡ ℂ fld ∧ 1 ∈ A ∧ ∀ x ∈ A ∀ y ∈ A x ⁢ y ∈ A
13 8 12 ax-mp ⊢ A ∈ SubRing ⁡ ℂ fld ↔ A ∈ SubGrp ⁡ ℂ fld ∧ 1 ∈ A ∧ ∀ x ∈ A ∀ y ∈ A x ⁢ y ∈ A
14 6 4 7 13 mpbir3an ⊢ A ∈ SubRing ⁡ ℂ fld