Metamath Proof Explorer

Theorem cnsubdrglem

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

Ref Expression
Hypotheses cnsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
cnsubglem.2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
cnsubglem.3 ⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
cnsubrglem.4 ⊢ 1 ∈ 𝐴
cnsubrglem.5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
cnsubrglem.6 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐴 )
Assertion cnsubdrglem ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐴 ) ∈ DivRing )

Proof

Step Hyp Ref Expression
1 cnsubglem.1 ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℂ )
2 cnsubglem.2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 + 𝑦 ) ∈ 𝐴 )
3 cnsubglem.3 ⊢ ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ 𝐴 )
4 cnsubrglem.4 ⊢ 1 ∈ 𝐴
5 cnsubrglem.5 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 · 𝑦 ) ∈ 𝐴 )
6 cnsubrglem.6 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐴 )
7 1 2 3 4 5 cnsubrglem ⊢ 𝐴 ∈ ( SubRing ‘ ℂfld )
8 cndrng ⊢ ℂfld ∈ DivRing
9 eqid ⊢ ( ℂfld ↾s 𝐴 ) = ( ℂfld ↾s 𝐴 )
10 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
11 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
12 9 10 11 issubdrg ⊢ ( ( ℂfld ∈ DivRing ∧ 𝐴 ∈ ( SubRing ‘ ℂfld ) ) → ( ( ℂfld ↾s 𝐴 ) ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 ) )
13 8 7 12 mp2an ⊢ ( ( ℂfld ↾s 𝐴 ) ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
14 cnring ⊢ ℂfld ∈ Ring
15 1 ssriv ⊢ 𝐴 ⊆ ℂ
16 ssdif ⊢ ( 𝐴 ⊆ ℂ → ( 𝐴 ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } ) )
17 15 16 ax-mp ⊢ ( 𝐴 ∖ { 0 } ) ⊆ ( ℂ ∖ { 0 } )
18 17 sseli ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
19 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
20 19 10 8 drngui ⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
21 cnflddiv ⊢ / = ( /r ‘ ℂfld )
22 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
23 19 20 21 22 11 ringinvdv ⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
24 14 18 23 sylancr ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
25 eldifsn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0 ) )
26 25 6 sylbi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ 𝐴 )
27 24 26 eqeltrd ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 0 } ) → ( ( invr ‘ ℂfld ) ‘ 𝑥 ) ∈ 𝐴 )
28 13 27 mprgbir ⊢ ( ℂfld ↾s 𝐴 ) ∈ DivRing
29 7 28 pm3.2i ⊢ ( 𝐴 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐴 ) ∈ DivRing )