# Metamath Proof Explorer

## Theorem primefld

Description: The smallest sub division ring of a division ring, here named P , is a field, called thePrime Field of R . (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis primefld.1 ${⊢}{P}={R}{↾}_{𝑠}\bigcap \mathrm{SubDRing}\left({R}\right)$
Assertion primefld ${⊢}{R}\in \mathrm{DivRing}\to {P}\in \mathrm{Field}$

### Proof

Step Hyp Ref Expression
1 primefld.1 ${⊢}{P}={R}{↾}_{𝑠}\bigcap \mathrm{SubDRing}\left({R}\right)$
2 id ${⊢}{R}\in \mathrm{DivRing}\to {R}\in \mathrm{DivRing}$
3 issdrg ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)↔\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubRing}\left({R}\right)\wedge {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}\right)$
4 3 simp2bi ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)\to {s}\in \mathrm{SubRing}\left({R}\right)$
5 4 ssriv ${⊢}\mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{SubRing}\left({R}\right)$
6 5 a1i ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{SubRing}\left({R}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
8 7 sdrgid ${⊢}{R}\in \mathrm{DivRing}\to {\mathrm{Base}}_{{R}}\in \mathrm{SubDRing}\left({R}\right)$
9 8 ne0d ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\ne \varnothing$
10 3 simp3bi ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)\to {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
11 10 adantl ${⊢}\left({R}\in \mathrm{DivRing}\wedge {s}\in \mathrm{SubDRing}\left({R}\right)\right)\to {R}{↾}_{𝑠}{s}\in \mathrm{DivRing}$
12 1 2 6 9 11 subdrgint ${⊢}{R}\in \mathrm{DivRing}\to {P}\in \mathrm{DivRing}$
13 drngring ${⊢}{P}\in \mathrm{DivRing}\to {P}\in \mathrm{Ring}$
14 12 13 syl ${⊢}{R}\in \mathrm{DivRing}\to {P}\in \mathrm{Ring}$
15 ssidd ${⊢}{R}\in \mathrm{DivRing}\to {\mathrm{Base}}_{{R}}\subseteq {\mathrm{Base}}_{{R}}$
16 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
17 eqid ${⊢}\mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)=\mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)$
18 7 16 17 cntzsdrg ${⊢}\left({R}\in \mathrm{DivRing}\wedge {\mathrm{Base}}_{{R}}\subseteq {\mathrm{Base}}_{{R}}\right)\to \mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)\in \mathrm{SubDRing}\left({R}\right)$
19 2 15 18 syl2anc ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)\in \mathrm{SubDRing}\left({R}\right)$
20 intss1 ${⊢}\mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)\in \mathrm{SubDRing}\left({R}\right)\to \bigcap \mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)$
21 19 20 syl ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)$
22 16 7 mgpbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{R}}}$
23 22 17 cntrval ${⊢}\mathrm{Cntz}\left({\mathrm{mulGrp}}_{{R}}\right)\left({\mathrm{Base}}_{{R}}\right)=\mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
24 21 23 sseqtrdi ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
25 22 cntrss ${⊢}\mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)\subseteq {\mathrm{Base}}_{{R}}$
26 24 25 sstrdi ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)\subseteq {\mathrm{Base}}_{{R}}$
27 1 7 ressbas2 ${⊢}\bigcap \mathrm{SubDRing}\left({R}\right)\subseteq {\mathrm{Base}}_{{R}}\to \bigcap \mathrm{SubDRing}\left({R}\right)={\mathrm{Base}}_{{P}}$
28 26 27 syl ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)={\mathrm{Base}}_{{P}}$
29 28 24 eqsstrrd ${⊢}{R}\in \mathrm{DivRing}\to {\mathrm{Base}}_{{P}}\subseteq \mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
30 29 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {\mathrm{Base}}_{{P}}\subseteq \mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
31 simprl ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}\in {\mathrm{Base}}_{{P}}$
32 30 31 sseldd ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}\in \mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
33 28 26 eqsstrrd ${⊢}{R}\in \mathrm{DivRing}\to {\mathrm{Base}}_{{P}}\subseteq {\mathrm{Base}}_{{R}}$
34 33 adantr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {\mathrm{Base}}_{{P}}\subseteq {\mathrm{Base}}_{{R}}$
35 simprr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {y}\in {\mathrm{Base}}_{{P}}$
36 34 35 sseldd ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {y}\in {\mathrm{Base}}_{{R}}$
37 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
38 16 37 mgpplusg ${⊢}{\cdot }_{{R}}={+}_{{\mathrm{mulGrp}}_{{R}}}$
39 eqid ${⊢}\mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)=\mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)$
40 22 38 39 cntri ${⊢}\left({x}\in \mathrm{Cntr}\left({\mathrm{mulGrp}}_{{R}}\right)\wedge {y}\in {\mathrm{Base}}_{{R}}\right)\to {x}{\cdot }_{{R}}{y}={y}{\cdot }_{{R}}{x}$
41 32 36 40 syl2anc ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}{\cdot }_{{R}}{y}={y}{\cdot }_{{R}}{x}$
42 8 26 ssexd ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)\in \mathrm{V}$
43 1 37 ressmulr ${⊢}\bigcap \mathrm{SubDRing}\left({R}\right)\in \mathrm{V}\to {\cdot }_{{R}}={\cdot }_{{P}}$
44 42 43 syl ${⊢}{R}\in \mathrm{DivRing}\to {\cdot }_{{R}}={\cdot }_{{P}}$
45 44 oveqdr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}{\cdot }_{{R}}{y}={x}{\cdot }_{{P}}{y}$
46 44 oveqdr ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {y}{\cdot }_{{R}}{x}={y}{\cdot }_{{P}}{x}$
47 41 45 46 3eqtr3d ${⊢}\left({R}\in \mathrm{DivRing}\wedge \left({x}\in {\mathrm{Base}}_{{P}}\wedge {y}\in {\mathrm{Base}}_{{P}}\right)\right)\to {x}{\cdot }_{{P}}{y}={y}{\cdot }_{{P}}{x}$
48 47 ralrimivva ${⊢}{R}\in \mathrm{DivRing}\to \forall {x}\in {\mathrm{Base}}_{{P}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{P}}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{P}}{y}={y}{\cdot }_{{P}}{x}$
49 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
50 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
51 49 50 iscrng2 ${⊢}{P}\in \mathrm{CRing}↔\left({P}\in \mathrm{Ring}\wedge \forall {x}\in {\mathrm{Base}}_{{P}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{P}}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{P}}{y}={y}{\cdot }_{{P}}{x}\right)$
52 14 48 51 sylanbrc ${⊢}{R}\in \mathrm{DivRing}\to {P}\in \mathrm{CRing}$
53 isfld ${⊢}{P}\in \mathrm{Field}↔\left({P}\in \mathrm{DivRing}\wedge {P}\in \mathrm{CRing}\right)$
54 12 52 53 sylanbrc ${⊢}{R}\in \mathrm{DivRing}\to {P}\in \mathrm{Field}$