Metamath Proof Explorer

Theorem cnsubglem

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

Ref Expression
Hypotheses cnsubglem.1 ⊢ x ∈ A → x ∈ ℂ
cnsubglem.2 ⊢ x ∈ A ∧ y ∈ A → x + y ∈ A
cnsubglem.3 ⊢ x ∈ A → − x ∈ A
cnsubglem.4 ⊢ B ∈ A
Assertion cnsubglem ⊢ A ∈ SubGrp ⁡ ℂ 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 cnsubglem.4 ⊢ B ∈ A
5 1 ssriv ⊢ A ⊆ ℂ
6 4 ne0ii ⊢ A ≠ ∅
7 2 ralrimiva ⊢ x ∈ A → ∀ y ∈ A x + y ∈ A
8 cnfldneg ⊢ x ∈ ℂ → inv g ⁡ ℂ fld ⁡ x = − x
9 1 8 syl ⊢ x ∈ A → inv g ⁡ ℂ fld ⁡ x = − x
10 9 3 eqeltrd ⊢ x ∈ A → inv g ⁡ ℂ fld ⁡ x ∈ A
11 7 10 jca ⊢ x ∈ A → ∀ y ∈ A x + y ∈ A ∧ inv g ⁡ ℂ fld ⁡ x ∈ A
12 11 rgen ⊢ ∀ x ∈ A ∀ y ∈ A x + y ∈ A ∧ inv g ⁡ ℂ fld ⁡ x ∈ A
13 cnring ⊢ ℂ fld ∈ Ring
14 ringgrp ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Grp
15 cnfldbas ⊢ ℂ = Base ℂ fld
16 cnfldadd ⊢ + = + ℂ fld
17 eqid ⊢ inv g ⁡ ℂ fld = inv g ⁡ ℂ fld
18 15 16 17 issubg2 ⊢ ℂ fld ∈ Grp → A ∈ SubGrp ⁡ ℂ fld ↔ A ⊆ ℂ ∧ A ≠ ∅ ∧ ∀ x ∈ A ∀ y ∈ A x + y ∈ A ∧ inv g ⁡ ℂ fld ⁡ x ∈ A
19 13 14 18 mp2b ⊢ A ∈ SubGrp ⁡ ℂ fld ↔ A ⊆ ℂ ∧ A ≠ ∅ ∧ ∀ x ∈ A ∀ y ∈ A x + y ∈ A ∧ inv g ⁡ ℂ fld ⁡ x ∈ A
20 5 6 12 19 mpbir3an ⊢ A ∈ SubGrp ⁡ ℂ fld