primefld0cl

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

		Ref	Expression
	Hypothesis	primefld0cl.1	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	primefld0cl	$⊢ R \in DivRing \to \underset{˙}{0} \in ⋂ SubDRing (R)$

Step	Hyp	Ref	Expression
1		primefld0cl.1	$⊢ \underset{˙}{0} = 0_{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		subrgsubg	$⊢ s \in SubRing (R) \to s \in SubGrp (R)$
5	3 4	syl	$⊢ s \in SubDRing (R) \to s \in SubGrp (R)$
6	5	a1i	$⊢ R \in DivRing \to (s \in SubDRing (R) \to s \in SubGrp (R))$
7	6	ssrdv	$⊢ R \in DivRing \to SubDRing (R) \subseteq SubGrp (R)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8	sdrgid	$⊢ R \in DivRing \to {Base}_{R} \in SubDRing (R)$
10	9	ne0d	$⊢ R \in DivRing \to SubDRing (R) \neq \emptyset$
11		subgint	$⊢ (SubDRing (R) \subseteq SubGrp (R) \land SubDRing (R) \neq \emptyset) \to ⋂ SubDRing (R) \in SubGrp (R)$
12	7 10 11	syl2anc	$⊢ R \in DivRing \to ⋂ SubDRing (R) \in SubGrp (R)$
13	1	subg0cl	$⊢ ⋂ SubDRing (R) \in SubGrp (R) \to \underset{˙}{0} \in ⋂ SubDRing (R)$
14	12 13	syl	$⊢ R \in DivRing \to \underset{˙}{0} \in ⋂ SubDRing (R)$

Metamath Proof Explorer