Metamath Proof Explorer

Theorem primefld

Description: The smallest sub division ring of a division ring, here named P , is a field, called thePrime Field of R . (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Hypothesis primefld.1 
|- P = ( R |`s |^| ( SubDRing ` R ) )
Assertion primefld 
|- ( R e. DivRing -> P e. Field )

Proof

Step Hyp Ref Expression
1 primefld.1 
 |-  P = ( R |`s |^| ( SubDRing ` R ) )
2 id 
 |-  ( R e. DivRing -> R e. DivRing )
3 issdrg 
 |-  ( s e. ( SubDRing ` R ) <-> ( R e. DivRing /\ s e. ( SubRing ` R ) /\ ( R |`s s ) e. DivRing ) )
4 3 simp2bi 
 |-  ( s e. ( SubDRing ` R ) -> s e. ( SubRing ` R ) )
5 4 ssriv 
 |-  ( SubDRing ` R ) C_ ( SubRing ` R )
6 5 a1i 
 |-  ( R e. DivRing -> ( SubDRing ` R ) C_ ( SubRing ` R ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 7 sdrgid 
 |-  ( R e. DivRing -> ( Base ` R ) e. ( SubDRing ` R ) )
9 8 ne0d 
 |-  ( R e. DivRing -> ( SubDRing ` R ) =/= (/) )
10 3 simp3bi 
 |-  ( s e. ( SubDRing ` R ) -> ( R |`s s ) e. DivRing )
11 10 adantl 
 |-  ( ( R e. DivRing /\ s e. ( SubDRing ` R ) ) -> ( R |`s s ) e. DivRing )
12 1 2 6 9 11 subdrgint 
 |-  ( R e. DivRing -> P e. DivRing )
13 drngring 
 |-  ( P e. DivRing -> P e. Ring )
14 12 13 syl 
 |-  ( R e. DivRing -> P e. Ring )
15 ssidd 
 |-  ( R e. DivRing -> ( Base ` R ) C_ ( Base ` R ) )
16 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
17 eqid 
 |-  ( Cntz ` ( mulGrp ` R ) ) = ( Cntz ` ( mulGrp ` R ) )
18 7 16 17 cntzsdrg 
 |-  ( ( R e. DivRing /\ ( Base ` R ) C_ ( Base ` R ) ) -> ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) e. ( SubDRing ` R ) )
19 2 15 18 syl2anc 
 |-  ( R e. DivRing -> ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) e. ( SubDRing ` R ) )
20 intss1 
 |-  ( ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) e. ( SubDRing ` R ) -> |^| ( SubDRing ` R ) C_ ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) )
21 19 20 syl 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) C_ ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) )
22 16 7 mgpbas 
 |-  ( Base ` R ) = ( Base ` ( mulGrp ` R ) )
23 22 17 cntrval 
 |-  ( ( Cntz ` ( mulGrp ` R ) ) ` ( Base ` R ) ) = ( Cntr ` ( mulGrp ` R ) )
24 21 23 sseqtrdi 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) C_ ( Cntr ` ( mulGrp ` R ) ) )
25 22 cntrss 
 |-  ( Cntr ` ( mulGrp ` R ) ) C_ ( Base ` R )
26 24 25 sstrdi 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) C_ ( Base ` R ) )
27 1 7 ressbas2 
 |-  ( |^| ( SubDRing ` R ) C_ ( Base ` R ) -> |^| ( SubDRing ` R ) = ( Base ` P ) )
28 26 27 syl 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) = ( Base ` P ) )
29 28 24 eqsstrrd 
 |-  ( R e. DivRing -> ( Base ` P ) C_ ( Cntr ` ( mulGrp ` R ) ) )
30 29 adantr 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( Base ` P ) C_ ( Cntr ` ( mulGrp ` R ) ) )
31 simprl 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> x e. ( Base ` P ) )
32 30 31 sseldd 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> x e. ( Cntr ` ( mulGrp ` R ) ) )
33 28 26 eqsstrrd 
 |-  ( R e. DivRing -> ( Base ` P ) C_ ( Base ` R ) )
34 33 adantr 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( Base ` P ) C_ ( Base ` R ) )
35 simprr 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> y e. ( Base ` P ) )
36 34 35 sseldd 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> y e. ( Base ` R ) )
37 eqid 
 |-  ( .r ` R ) = ( .r ` R )
38 16 37 mgpplusg 
 |-  ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
39 eqid 
 |-  ( Cntr ` ( mulGrp ` R ) ) = ( Cntr ` ( mulGrp ` R ) )
40 22 38 39 cntri 
 |-  ( ( x e. ( Cntr ` ( mulGrp ` R ) ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) = ( y ( .r ` R ) x ) )
41 32 36 40 syl2anc 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` R ) y ) = ( y ( .r ` R ) x ) )
42 8 26 ssexd 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) e. _V )
43 1 37 ressmulr 
 |-  ( |^| ( SubDRing ` R ) e. _V -> ( .r ` R ) = ( .r ` P ) )
44 42 43 syl 
 |-  ( R e. DivRing -> ( .r ` R ) = ( .r ` P ) )
45 44 oveqdr 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` P ) y ) )
46 44 oveqdr 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( y ( .r ` R ) x ) = ( y ( .r ` P ) x ) )
47 41 45 46 3eqtr3d 
 |-  ( ( R e. DivRing /\ ( x e. ( Base ` P ) /\ y e. ( Base ` P ) ) ) -> ( x ( .r ` P ) y ) = ( y ( .r ` P ) x ) )
48 47 ralrimivva 
 |-  ( R e. DivRing -> A. x e. ( Base ` P ) A. y e. ( Base ` P ) ( x ( .r ` P ) y ) = ( y ( .r ` P ) x ) )
49 eqid 
 |-  ( Base ` P ) = ( Base ` P )
50 eqid 
 |-  ( .r ` P ) = ( .r ` P )
51 49 50 iscrng2 
 |-  ( P e. CRing <-> ( P e. Ring /\ A. x e. ( Base ` P ) A. y e. ( Base ` P ) ( x ( .r ` P ) y ) = ( y ( .r ` P ) x ) ) )
52 14 48 51 sylanbrc 
 |-  ( R e. DivRing -> P e. CRing )
53 isfld 
 |-  ( P e. Field <-> ( P e. DivRing /\ P e. CRing ) )
54 12 52 53 sylanbrc 
 |-  ( R e. DivRing -> P e. Field )