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 = ( Poly1 ` R )
	ply1lvec.r	|- ( ph -> R e. DivRing )
Assertion	ply1lvec	|- ( ph -> P e. LVec )

Proof

Step	Hyp	Ref	Expression
1		ply1lvec.p	|- P = ( Poly1 ` R )
2		ply1lvec.r	|- ( ph -> R e. DivRing )
3	2	drngringd	|- ( ph -> R e. Ring )
4	1	ply1lmod	|- ( R e. Ring -> P e. LMod )
5	3 4	syl	|- ( ph -> P e. LMod )
6	1	ply1sca	|- ( R e. DivRing -> R = ( Scalar ` P ) )
7	2 6	syl	|- ( ph -> R = ( Scalar ` P ) )
8	7 2	eqeltrrd	|- ( ph -> ( Scalar ` P ) e. DivRing )
9		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
10	9	islvec	|- ( P e. LVec <-> ( P e. LMod /\ ( Scalar ` P ) e. DivRing ) )
11	5 8 10	sylanbrc	|- ( ph -> P e. LVec )