Metamath Proof Explorer

Theorem cnsubdrglem

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
cnsubrglem.4 ⊢ 1 ∈ A
cnsubrglem.5 ⊢ x ∈ A ∧ y ∈ A → x ⁢ y ∈ A
cnsubrglem.6 ⊢ x ∈ A ∧ x ≠ 0 → 1 x ∈ A
Assertion cnsubdrglem ⊢ A ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 A ∈ DivRing

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 cnsubrglem.6 ⊢ x ∈ A ∧ x ≠ 0 → 1 x ∈ A
7 1 2 3 4 5 cnsubrglem ⊢ A ∈ SubRing ⁡ ℂ fld
8 cndrng ⊢ ℂ fld ∈ DivRing
9 eqid ⊢ ℂ fld ↾ 𝑠 A = ℂ fld ↾ 𝑠 A
10 cnfld0 ⊢ 0 = 0 ℂ fld
11 eqid ⊢ inv r ⁡ ℂ fld = inv r ⁡ ℂ fld
12 9 10 11 issubdrg ⊢ ℂ fld ∈ DivRing ∧ A ∈ SubRing ⁡ ℂ fld → ℂ fld ↾ 𝑠 A ∈ DivRing ↔ ∀ x ∈ A ∖ 0 inv r ⁡ ℂ fld ⁡ x ∈ A
13 8 7 12 mp2an ⊢ ℂ fld ↾ 𝑠 A ∈ DivRing ↔ ∀ x ∈ A ∖ 0 inv r ⁡ ℂ fld ⁡ x ∈ A
14 cnring ⊢ ℂ fld ∈ Ring
15 1 ssriv ⊢ A ⊆ ℂ
16 ssdif ⊢ A ⊆ ℂ → A ∖ 0 ⊆ ℂ ∖ 0
17 15 16 ax-mp ⊢ A ∖ 0 ⊆ ℂ ∖ 0
18 17 sseli ⊢ x ∈ A ∖ 0 → x ∈ ℂ ∖ 0
19 cnfldbas ⊢ ℂ = Base ℂ fld
20 19 10 8 drngui ⊢ ℂ ∖ 0 = Unit ⁡ ℂ fld
21 cnflddiv ⊢ ÷ = / r ⁡ ℂ fld
22 cnfld1 ⊢ 1 = 1 ℂ fld
23 19 20 21 22 11 ringinvdv ⊢ ℂ fld ∈ Ring ∧ x ∈ ℂ ∖ 0 → inv r ⁡ ℂ fld ⁡ x = 1 x
24 14 18 23 sylancr ⊢ x ∈ A ∖ 0 → inv r ⁡ ℂ fld ⁡ x = 1 x
25 eldifsn ⊢ x ∈ A ∖ 0 ↔ x ∈ A ∧ x ≠ 0
26 25 6 sylbi ⊢ x ∈ A ∖ 0 → 1 x ∈ A
27 24 26 eqeltrd ⊢ x ∈ A ∖ 0 → inv r ⁡ ℂ fld ⁡ x ∈ A
28 13 27 mprgbir ⊢ ℂ fld ↾ 𝑠 A ∈ DivRing
29 7 28 pm3.2i ⊢ A ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 A ∈ DivRing