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

Metamath Proof Explorer

Theorem ply1lvec

Description: In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025)

Ref Expression
Hypotheses ply1lvec.p ⊢ P = Poly 1 ⁡ R
ply1lvec.r ⊢ φ → R ∈ DivRing
Assertion ply1lvec ⊢ φ → P ∈ LVec

Proof

Step Hyp Ref Expression
1 ply1lvec.p ⊢ P = Poly 1 ⁡ R
2 ply1lvec.r ⊢ φ → R ∈ DivRing
3 2 drngringd ⊢ φ → R ∈ Ring
4 1 ply1lmod ⊢ R ∈ Ring → P ∈ LMod
5 3 4 syl ⊢ φ → P ∈ LMod
6 1 ply1sca ⊢ R ∈ DivRing → R = Scalar ⁡ P
7 2 6 syl ⊢ φ → R = Scalar ⁡ P
8 7 2 eqeltrrd ⊢ φ → Scalar ⁡ P ∈ DivRing
9 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
10 9 islvec ⊢ P ∈ LVec ↔ P ∈ LMod ∧ Scalar ⁡ P ∈ DivRing
11 5 8 10 sylanbrc ⊢ φ → P ∈ LVec