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

Metamath Proof Explorer

Theorem fldextsubrg

Description: Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Hypothesis fldextsubrg.1 ⊢ U = Base F
Assertion fldextsubrg ⊢ E /FldExt F → U ∈ SubRing ⁡ E

Proof

Step Hyp Ref Expression
1 fldextsubrg.1 ⊢ U = Base F
2 fldextfld1 ⊢ E /FldExt F → E ∈ Field
3 fldextfld2 ⊢ E /FldExt F → F ∈ Field
4 brfldext ⊢ E ∈ Field ∧ F ∈ Field → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
5 2 3 4 syl2anc ⊢ E /FldExt F → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
6 5 ibi ⊢ E /FldExt F → F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
7 6 simprd ⊢ E /FldExt F → Base F ∈ SubRing ⁡ E
8 1 7 eqeltrid ⊢ E /FldExt F → U ∈ SubRing ⁡ E