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	⊢ 𝑃 = ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) )
Assertion	primefldchr	⊢ ( 𝑅 ∈ DivRing → ( chr ‘ 𝑃 ) = ( chr ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		primefldchr.1	⊢ 𝑃 = ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) )
2	1	fveq2i	⊢ ( chr ‘ 𝑃 ) = ( chr ‘ ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) ) )
3		issdrg	⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑠 ) ∈ DivRing ) )
4	3	simp2bi	⊢ ( 𝑠 ∈ ( SubDRing ‘ 𝑅 ) → 𝑠 ∈ ( SubRing ‘ 𝑅 ) )
5	4	ssriv	⊢ ( SubDRing ‘ 𝑅 ) ⊆ ( SubRing ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	6	sdrgid	⊢ ( 𝑅 ∈ DivRing → ( Base ‘ 𝑅 ) ∈ ( SubDRing ‘ 𝑅 ) )
8	7	ne0d	⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) ≠ ∅ )
9		subrgint	⊢ ( ( ( SubDRing ‘ 𝑅 ) ⊆ ( SubRing ‘ 𝑅 ) ∧ ( SubDRing ‘ 𝑅 ) ≠ ∅ ) → ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
10	5 8 9	sylancr	⊢ ( 𝑅 ∈ DivRing → ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
11		subrgchr	⊢ ( ∩ ( SubDRing ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) → ( chr ‘ ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) ) ) = ( chr ‘ 𝑅 ) )
12	10 11	syl	⊢ ( 𝑅 ∈ DivRing → ( chr ‘ ( 𝑅 ↾s ∩ ( SubDRing ‘ 𝑅 ) ) ) = ( chr ‘ 𝑅 ) )
13	2 12	eqtrid	⊢ ( 𝑅 ∈ DivRing → ( chr ‘ 𝑃 ) = ( chr ‘ 𝑅 ) )