# Metamath Proof Explorer

## Theorem issubdrg

Description: Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubdrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
issubdrg.z
issubdrg.i ${⊢}{I}={inv}_{r}\left({R}\right)$
Assertion issubdrg

### Proof

Step Hyp Ref Expression
1 issubdrg.s ${⊢}{S}={R}{↾}_{𝑠}{A}$
2 issubdrg.z
3 issubdrg.i ${⊢}{I}={inv}_{r}\left({R}\right)$
4 simpllr
5 1 subrgring ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {S}\in \mathrm{Ring}$
6 4 5 syl
7 simpr
8 eldifsn
9 7 8 sylib
10 9 simpld
11 1 subrgbas ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}={\mathrm{Base}}_{{S}}$
12 4 11 syl
13 10 12 eleqtrd
14 9 simprd
15 1 2 subrg0
16 4 15 syl
17 14 16 neeqtrd
18 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
19 eqid ${⊢}\mathrm{Unit}\left({S}\right)=\mathrm{Unit}\left({S}\right)$
20 eqid ${⊢}{0}_{{S}}={0}_{{S}}$
21 18 19 20 drngunit ${⊢}{S}\in \mathrm{DivRing}\to \left({x}\in \mathrm{Unit}\left({S}\right)↔\left({x}\in {\mathrm{Base}}_{{S}}\wedge {x}\ne {0}_{{S}}\right)\right)$
22 21 ad2antlr
23 13 17 22 mpbir2and
24 eqid ${⊢}{inv}_{r}\left({S}\right)={inv}_{r}\left({S}\right)$
25 19 24 18 ringinvcl ${⊢}\left({S}\in \mathrm{Ring}\wedge {x}\in \mathrm{Unit}\left({S}\right)\right)\to {inv}_{r}\left({S}\right)\left({x}\right)\in {\mathrm{Base}}_{{S}}$
26 6 23 25 syl2anc
27 1 3 19 24 subrginv ${⊢}\left({A}\in \mathrm{SubRing}\left({R}\right)\wedge {x}\in \mathrm{Unit}\left({S}\right)\right)\to {I}\left({x}\right)={inv}_{r}\left({S}\right)\left({x}\right)$
28 4 23 27 syl2anc
29 26 28 12 3eltr4d
30 29 ralrimiva
31 5 ad2antlr
32 eqid ${⊢}\mathrm{Unit}\left({R}\right)=\mathrm{Unit}\left({R}\right)$
33 1 32 19 subrguss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \mathrm{Unit}\left({S}\right)\subseteq \mathrm{Unit}\left({R}\right)$
34 33 ad2antlr
35 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
36 35 32 2 isdrng
37 36 simprbi
38 37 ad2antrr
39 34 38 sseqtrd
40 18 19 unitss ${⊢}\mathrm{Unit}\left({S}\right)\subseteq {\mathrm{Base}}_{{S}}$
41 11 ad2antlr
42 40 41 sseqtrrid
43 39 42 ssind
44 35 subrgss ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to {A}\subseteq {\mathrm{Base}}_{{R}}$
45 44 ad2antlr
46 difin2
47 45 46 syl
48 43 47 sseqtrrd
49 44 ad2antlr
50 simprl
51 50 8 sylib
52 51 simpld
53 49 52 sseldd
54 51 simprd
55 35 32 2 drngunit
56 55 ad2antrr
57 53 54 56 mpbir2and
58 simprr
59 1 32 19 3 subrgunit ${⊢}{A}\in \mathrm{SubRing}\left({R}\right)\to \left({x}\in \mathrm{Unit}\left({S}\right)↔\left({x}\in \mathrm{Unit}\left({R}\right)\wedge {x}\in {A}\wedge {I}\left({x}\right)\in {A}\right)\right)$
60 59 ad2antlr
61 57 52 58 60 mpbir3and
62 61 expr
63 62 ralimdva
64 63 imp
65 dfss3
66 64 65 sylibr
67 48 66 eqssd
68 15 ad2antlr
69 68 sneqd
70 41 69 difeq12d
71 67 70 eqtrd
72 18 19 20 isdrng ${⊢}{S}\in \mathrm{DivRing}↔\left({S}\in \mathrm{Ring}\wedge \mathrm{Unit}\left({S}\right)={\mathrm{Base}}_{{S}}\setminus \left\{{0}_{{S}}\right\}\right)$
73 31 71 72 sylanbrc
74 30 73 impbida