Theorem fldextchr

Description: The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023)

	Ref	Expression
Assertion	fldextchr	$$⊢E{/}_{\mathrm{FldExt}}F\to \mathrm{chr}\left(F\right)=\mathrm{chr}\left(E\right)$$

Proof

Step	Hyp	Ref	Expression
1		fldextress	$$⊢E{/}_{\mathrm{FldExt}}F\to F=E{\upharpoonright }_{𝑠}{\mathrm{Base}}_F$$
2	1	fveq2d	$$⊢E{/}_{\mathrm{FldExt}}F\to \mathrm{chr}\left(F\right)=\mathrm{chr}\left(E{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)$$
3		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
4	3	fldextsubrg	$$⊢E{/}_{\mathrm{FldExt}}F\to {\mathrm{Base}}_F\in \mathrm{SubRing}\left(E\right)$$
5		subrgchr	$$⊢{\mathrm{Base}}_F\in \mathrm{SubRing}\left(E\right)\to \mathrm{chr}\left(E{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)=\mathrm{chr}\left(E\right)$$
6	4 5	syl	$$⊢E{/}_{\mathrm{FldExt}}F\to \mathrm{chr}\left(E{\upharpoonright }_{𝑠}{\mathrm{Base}}_F\right)=\mathrm{chr}\left(E\right)$$
7	2 6	eqtrd	$$⊢E{/}_{\mathrm{FldExt}}F\to \mathrm{chr}\left(F\right)=\mathrm{chr}\left(E\right)$$