Metamath Proof Explorer

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 ` R )
Assertion primefld0cl 
|- ( R e. DivRing -> .0. e. |^| ( SubDRing ` R ) )

Proof

Step Hyp Ref Expression
1 primefld0cl.1 
 |-  .0. = ( 0g ` R )
2 issdrg 
 |-  ( s e. ( SubDRing ` R ) <-> ( R e. DivRing /\ s e. ( SubRing ` R ) /\ ( R |`s s ) e. DivRing ) )
3 2 simp2bi 
 |-  ( s e. ( SubDRing ` R ) -> s e. ( SubRing ` R ) )
4 subrgsubg 
 |-  ( s e. ( SubRing ` R ) -> s e. ( SubGrp ` R ) )
5 3 4 syl 
 |-  ( s e. ( SubDRing ` R ) -> s e. ( SubGrp ` R ) )
6 5 a1i 
 |-  ( R e. DivRing -> ( s e. ( SubDRing ` R ) -> s e. ( SubGrp ` R ) ) )
7 6 ssrdv 
 |-  ( R e. DivRing -> ( SubDRing ` R ) C_ ( SubGrp ` R ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 8 sdrgid 
 |-  ( R e. DivRing -> ( Base ` R ) e. ( SubDRing ` R ) )
10 9 ne0d 
 |-  ( R e. DivRing -> ( SubDRing ` R ) =/= (/) )
11 subgint 
 |-  ( ( ( SubDRing ` R ) C_ ( SubGrp ` R ) /\ ( SubDRing ` R ) =/= (/) ) -> |^| ( SubDRing ` R ) e. ( SubGrp ` R ) )
12 7 10 11 syl2anc 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) e. ( SubGrp ` R ) )
13 1 subg0cl 
 |-  ( |^| ( SubDRing ` R ) e. ( SubGrp ` R ) -> .0. e. |^| ( SubDRing ` R ) )
14 12 13 syl 
 |-  ( R e. DivRing -> .0. e. |^| ( SubDRing ` R ) )