Metamath Proof Explorer

Theorem 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 
|- .1. = ( 1r ` R )
Assertion primefld1cl 
|- ( R e. DivRing -> .1. e. |^| ( SubDRing ` R ) )

Proof

Step Hyp Ref Expression
1 primefld1cl.1 
 |-  .1. = ( 1r ` 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 3 a1i 
 |-  ( R e. DivRing -> ( s e. ( SubDRing ` R ) -> s e. ( SubRing ` R ) ) )
5 4 ssrdv 
 |-  ( R e. DivRing -> ( SubDRing ` R ) C_ ( SubRing ` R ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 6 sdrgid 
 |-  ( R e. DivRing -> ( Base ` R ) e. ( SubDRing ` R ) )
8 7 ne0d 
 |-  ( R e. DivRing -> ( SubDRing ` R ) =/= (/) )
9 subrgint 
 |-  ( ( ( SubDRing ` R ) C_ ( SubRing ` R ) /\ ( SubDRing ` R ) =/= (/) ) -> |^| ( SubDRing ` R ) e. ( SubRing ` R ) )
10 5 8 9 syl2anc 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) e. ( SubRing ` R ) )
11 1 subrg1cl 
 |-  ( |^| ( SubDRing ` R ) e. ( SubRing ` R ) -> .1. e. |^| ( SubDRing ` R ) )
12 10 11 syl 
 |-  ( R e. DivRing -> .1. e. |^| ( SubDRing ` R ) )