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={\mathrm{Poly}}_1\left(R\right)$$
	ply1lvec.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
Assertion	ply1lvec	$$⊢\phi \to P\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		ply1lvec.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1lvec.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
3	2	drngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
4	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
5	3 4	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
6	1	ply1sca	$$⊢R\in \mathrm{DivRing}\to R=\mathrm{Scalar}\left(P\right)$$
7	2 6	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
8	7 2	eqeltrrd	$$⊢\phi \to \mathrm{Scalar}\left(P\right)\in \mathrm{DivRing}$$
9		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
10	9	islvec	$$⊢P\in \mathrm{LVec}\leftrightarrow \left(P\in \mathrm{LMod}\wedge \mathrm{Scalar}\left(P\right)\in \mathrm{DivRing}\right)$$
11	5 8 10	sylanbrc	$$⊢\phi \to P\in \mathrm{LVec}$$