Metamath Proof Explorer

Theorem primefld1cl

Description: The prime field contains the multiplicative neutral element of the division ring. (Contributed by Thierry Arnoux, 22-Aug-2023)

Ref Expression
Hypothesis primefld1cl.1
Assertion primefld1cl

Proof

Step Hyp Ref Expression
1 primefld1cl.1
2 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)$
3 2 simp2bi ${⊢}{s}\in \mathrm{SubDRing}\left({R}\right)\to {s}\in \mathrm{SubRing}\left({R}\right)$
4 3 a1i ${⊢}{R}\in \mathrm{DivRing}\to \left({s}\in \mathrm{SubDRing}\left({R}\right)\to {s}\in \mathrm{SubRing}\left({R}\right)\right)$
5 4 ssrdv ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{SubRing}\left({R}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
7 6 sdrgid ${⊢}{R}\in \mathrm{DivRing}\to {\mathrm{Base}}_{{R}}\in \mathrm{SubDRing}\left({R}\right)$
8 7 ne0d ${⊢}{R}\in \mathrm{DivRing}\to \mathrm{SubDRing}\left({R}\right)\ne \varnothing$
9 subrgint ${⊢}\left(\mathrm{SubDRing}\left({R}\right)\subseteq \mathrm{SubRing}\left({R}\right)\wedge \mathrm{SubDRing}\left({R}\right)\ne \varnothing \right)\to \bigcap \mathrm{SubDRing}\left({R}\right)\in \mathrm{SubRing}\left({R}\right)$
10 5 8 9 syl2anc ${⊢}{R}\in \mathrm{DivRing}\to \bigcap \mathrm{SubDRing}\left({R}\right)\in \mathrm{SubRing}\left({R}\right)$
11 1 subrg1cl
12 10 11 syl