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