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 ↾_{𝑠} ⋂ SubDRing (R)$
	Assertion	primefldchr	$⊢ R \in DivRing \to chr (P) = chr (R)$

Proof

Step	Hyp	Ref	Expression
1		primefldchr.1	$⊢ P = R ↾_{𝑠} ⋂ SubDRing (R)$
2	1	fveq2i	$⊢ chr (P) = chr (R ↾_{𝑠} ⋂ SubDRing (R))$
3		issdrg	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land s \in SubRing (R) \land R ↾_{𝑠} s \in DivRing)$
4	3	simp2bi	$⊢ s \in SubDRing (R) \to s \in SubRing (R)$
5	4	ssriv	$⊢ SubDRing (R) \subseteq SubRing (R)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	6	sdrgid	$⊢ R \in DivRing \to {Base}_{R} \in SubDRing (R)$
8	7	ne0d	$⊢ R \in DivRing \to SubDRing (R) \neq \emptyset$
9		subrgint	$⊢ (SubDRing (R) \subseteq SubRing (R) \land SubDRing (R) \neq \emptyset) \to ⋂ SubDRing (R) \in SubRing (R)$
10	5 8 9	sylancr	$⊢ R \in DivRing \to ⋂ SubDRing (R) \in SubRing (R)$
11		subrgchr	$⊢ ⋂ SubDRing (R) \in SubRing (R) \to chr (R ↾_{𝑠} ⋂ SubDRing (R)) = chr (R)$
12	10 11	syl	$⊢ R \in DivRing \to chr (R ↾_{𝑠} ⋂ SubDRing (R)) = chr (R)$
13	2 12	eqtrid	$⊢ R \in DivRing \to chr (P) = chr (R)$