Metamath Proof Explorer


Theorem sralvec

Description: Given a sub division ring F of a division ring E , E may be considered as a vector space over F , which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023)

Ref Expression
Hypotheses sralvec.a A = subringAlg E U
sralvec.f F = E 𝑠 U
Assertion sralvec E DivRing F DivRing U SubRing E A LVec

Proof

Step Hyp Ref Expression
1 sralvec.a A = subringAlg E U
2 sralvec.f F = E 𝑠 U
3 eqid subringAlg E U = subringAlg E U
4 3 sralmod U SubRing E subringAlg E U LMod
5 4 3ad2ant3 E DivRing F DivRing U SubRing E subringAlg E U LMod
6 1 5 eqeltrid E DivRing F DivRing U SubRing E A LMod
7 1 a1i U SubRing E A = subringAlg E U
8 eqid Base E = Base E
9 8 subrgss U SubRing E U Base E
10 7 9 srasca U SubRing E E 𝑠 U = Scalar A
11 2 10 syl5eq U SubRing E F = Scalar A
12 11 3ad2ant3 E DivRing F DivRing U SubRing E F = Scalar A
13 simp2 E DivRing F DivRing U SubRing E F DivRing
14 12 13 eqeltrrd E DivRing F DivRing U SubRing E Scalar A DivRing
15 eqid Scalar A = Scalar A
16 15 islvec A LVec A LMod Scalar A DivRing
17 6 14 16 sylanbrc E DivRing F DivRing U SubRing E A LVec