Metamath Proof Explorer

Theorem fldextress

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

Ref Expression
Assertion fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F

Proof

Step Hyp Ref Expression
1 fldextfld1 ⊢ E /FldExt F → E ∈ Field
2 fldextfld2 ⊢ E /FldExt F → F ∈ Field
3 brfldext ⊢ E ∈ Field ∧ F ∈ Field → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
4 1 2 3 syl2anc ⊢ E /FldExt F → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
5 4 ibi ⊢ E /FldExt F → F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
6 5 simpld ⊢ E /FldExt F → F = E ↾ 𝑠 Base F