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 ⊢ 𝑃 = ( 𝑅 ↾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 ‘ 𝑅 ) )