This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 /FldExt F → chr ⁡ F = chr ⁡ E

Proof

Step Hyp Ref Expression
1 fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F
2 1 fveq2d ⊢ E /FldExt F → chr ⁡ F = chr ⁡ E ↾ 𝑠 Base F
3 eqid ⊢ Base F = Base F
4 3 fldextsubrg ⊢ E /FldExt F → Base F ∈ SubRing ⁡ E
5 subrgchr ⊢ Base F ∈ SubRing ⁡ E → chr ⁡ E ↾ 𝑠 Base F = chr ⁡ E
6 4 5 syl ⊢ E /FldExt F → chr ⁡ E ↾ 𝑠 Base F = chr ⁡ E
7 2 6 eqtrd ⊢ E /FldExt F → chr ⁡ F = chr ⁡ E