This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem primefld0cl

Description: The prime field contains the zero 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 ‘ 𝑅 ) )