Theorem 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	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	primefld0cl	⊢ ( 𝑅 ∈ DivRing → 0 ∈ ∩ ( SubDRing ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		primefld0cl.1	⊢ 0 = ( 0g ‘ 𝑅 )
2		issdrg	⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑠 ) ∈ DivRing ) )
3	2	simp2bi	⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubRing ‘ 𝑅 ) )
4		subrgsubg	⊢ ( 𝑠 ∈ ( SubRing ‘ 𝑅 ) → 𝑠 ∈ ( SubGrp ‘ 𝑅 ) )
5	3 4	syl	⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubGrp ‘ 𝑅 ) )
6	5	a1i	⊢ ( 𝑅 ∈ DivRing → ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubGrp ‘ 𝑅 ) ) )
7	6	ssrdv	⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 ) )
8		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9	8	sdrgid	⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑅 ) ∈ ( SubDRing ‘ 𝑅 ) )
10	9	ne0d	⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ≠ ∅ )
11		subgint	⊢ ( ( ( SubDRing ‘ 𝑅 ) ⊆ ( SubGrp ‘ 𝑅 ) ∧ ( SubDRing ‘ 𝑅 ) ≠ ∅ ) → ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubGrp ‘ 𝑅 ) )
12	7 10 11	syl2anc	⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubGrp ‘ 𝑅 ) )
13	1	subg0cl	⊢ ( ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubGrp ‘ 𝑅 ) → 0 ∈ ∩ ( SubDRing ‘ 𝑅 ) )
14	12 13	syl	⊢ ( 𝑅 ∈ DivRing → 0 ∈ ∩ ( SubDRing ‘ 𝑅 ) )