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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1lvec.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
Assertion	ply1lvec	⊢ ( 𝜑 → 𝑃 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		ply1lvec.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1lvec.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
3	2	drngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
5	3 4	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
6	1	ply1sca	⊢ ( 𝑅 ∈ DivRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
8	7 2	eqeltrrd	⊢ ( 𝜑 → ( Scalar ‘ 𝑃 ) ∈ DivRing )
9		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
10	9	islvec	⊢ ( 𝑃 ∈ LVec ↔ ( 𝑃 ∈ LMod ∧ ( Scalar ‘ 𝑃 ) ∈ DivRing ) )
11	5 8 10	sylanbrc	⊢ ( 𝜑 → 𝑃 ∈ LVec )