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	syl5eq	|- ( R e. DivRing -> ( chr ` P ) = ( chr ` R ) )