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

Metamath Proof Explorer

Theorem primefldchr

Description: The characteristic of a prime field is the same as the characteristic of the main field. (Contributed by Thierry Arnoux, 21-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 primefldchr.1 
 |-  P = ( R |`s |^| ( SubDRing ` R ) )
2 1 fveq2i 
 |-  ( chr ` P ) = ( chr ` ( R |`s |^| ( SubDRing ` R ) ) )
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 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 sylancr 
 |-  ( R e. DivRing -> |^| ( SubDRing ` R ) e. ( SubRing ` R ) )
11 subrgchr 
 |-  ( |^| ( SubDRing ` R ) e. ( SubRing ` R ) -> ( chr ` ( R |`s |^| ( SubDRing ` R ) ) ) = ( chr ` R ) )
12 10 11 syl 
 |-  ( R e. DivRing -> ( chr ` ( R |`s |^| ( SubDRing ` R ) ) ) = ( chr ` R ) )
13 2 12 eqtrid 
 |-  ( R e. DivRing -> ( chr ` P ) = ( chr ` R ) )