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	$⊢ \underset{˙}{1} = 1_{R}$
	Assertion	primefld1cl	$⊢ R \in DivRing \to \underset{˙}{1} \in ⋂ SubDRing (R)$

Step	Hyp	Ref	Expression
1		primefld1cl.1	$⊢ \underset{˙}{1} = 1_{R}$
2		issdrg	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land s \in SubRing (R) \land R ↾_{𝑠} s \in DivRing)$
3	2	simp2bi	$⊢ s \in SubDRing (R) \to s \in SubRing (R)$
4	3	a1i	$⊢ R \in DivRing \to (s \in SubDRing (R) \to s \in SubRing (R))$
5	4	ssrdv	$⊢ R \in DivRing \to SubDRing (R) \subseteq SubRing (R)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	6	sdrgid	$⊢ R \in DivRing \to {Base}_{R} \in SubDRing (R)$
8	7	ne0d	$⊢ R \in DivRing \to SubDRing (R) \neq \emptyset$
9		subrgint	$⊢ (SubDRing (R) \subseteq SubRing (R) \land SubDRing (R) \neq \emptyset) \to ⋂ SubDRing (R) \in SubRing (R)$
10	5 8 9	syl2anc	$⊢ R \in DivRing \to ⋂ SubDRing (R) \in SubRing (R)$
11	1	subrg1cl	$⊢ ⋂ SubDRing (R) \in SubRing (R) \to \underset{˙}{1} \in ⋂ SubDRing (R)$
12	10 11	syl	$⊢ R \in DivRing \to \underset{˙}{1} \in ⋂ SubDRing (R)$

Metamath Proof Explorer