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

Metamath Proof Explorer

Theorem fldextsralvec

Description: The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023)

Ref Expression
Assertion fldextsralvec ⊢ E /FldExt F → subringAlg ⁡ E ⁡ Base F ∈ LVec

Proof

Step Hyp Ref Expression
1 fldextfld1 ⊢ E /FldExt F → E ∈ Field
2 isfld ⊢ E ∈ Field ↔ E ∈ DivRing ∧ E ∈ CRing
3 1 2 sylib ⊢ E /FldExt F → E ∈ DivRing ∧ E ∈ CRing
4 3 simpld ⊢ E /FldExt F → E ∈ DivRing
5 fldextress ⊢ E /FldExt F → F = E ↾ 𝑠 Base F
6 fldextfld2 ⊢ E /FldExt F → F ∈ Field
7 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
8 6 7 sylib ⊢ E /FldExt F → F ∈ DivRing ∧ F ∈ CRing
9 8 simpld ⊢ E /FldExt F → F ∈ DivRing
10 5 9 eqeltrrd ⊢ E /FldExt F → E ↾ 𝑠 Base F ∈ DivRing
11 eqid ⊢ Base F = Base F
12 11 fldextsubrg ⊢ E /FldExt F → Base F ∈ SubRing ⁡ E
13 eqid ⊢ subringAlg ⁡ E ⁡ Base F = subringAlg ⁡ E ⁡ Base F
14 eqid ⊢ E ↾ 𝑠 Base F = E ↾ 𝑠 Base F
15 13 14 sralvec ⊢ E ∈ DivRing ∧ E ↾ 𝑠 Base F ∈ DivRing ∧ Base F ∈ SubRing ⁡ E → subringAlg ⁡ E ⁡ Base F ∈ LVec
16 4 10 12 15 syl3anc ⊢ E /FldExt F → subringAlg ⁡ E ⁡ Base F ∈ LVec