Metamath Proof Explorer

Theorem ply1lss

Description: Univariate polynomials form a linear subspace of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses ply1val.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1val.2 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
ply1bas.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
Assertion ply1lss ( 𝑅 ∈ Ring → 𝑈 ∈ ( LSubSp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ply1val.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1val.2 ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 )
3 ply1bas.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 eqid ⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6 1 2 3 ply1bas ⊢ 𝑈 = ( Base ‘ ( 1o mPoly 𝑅 ) )
7 1on ⊢ 1o ∈ On
8 7 a1i ⊢ ( 𝑅 ∈ Ring → 1o ∈ On )
9 id ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
10 4 5 6 8 9 mpllss ⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( LSubSp ‘ ( 1o mPwSer 𝑅 ) ) )
11 eqidd ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
12 2 psr1val ⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
13 0ss ⊢ ∅ ⊆ ( 1o × 1o )
14 13 a1i ⊢ ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) )
15 4 12 14 opsrbas ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ 𝑆 ) )
16 ssv ⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ⊆ V
17 16 a1i ⊢ ( 𝑅 ∈ Ring → ( Base ‘ ( 1o mPwSer 𝑅 ) ) ⊆ V )
18 4 12 14 opsrplusg ⊢ ( 𝑅 ∈ Ring → ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g ‘ 𝑆 ) )
19 18 oveqdr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
20 ovexd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) ∈ V )
21 4 12 14 opsrvsca ⊢ ( 𝑅 ∈ Ring → ( ·𝑠 ‘ ( 1o mPwSer 𝑅 ) ) = ( ·𝑠 ‘ 𝑆 ) )
22 21 oveqdr ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑆 ) 𝑦 ) )
23 4 8 9 psrsca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( 1o mPwSer 𝑅 ) ) )
24 23 fveq2d ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( 1o mPwSer 𝑅 ) ) ) )
25 4 12 14 8 9 opsrsca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑆 ) )
26 25 fveq2d ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑆 ) ) )
27 11 15 17 19 20 22 24 26 lsspropd ⊢ ( 𝑅 ∈ Ring → ( LSubSp ‘ ( 1o mPwSer 𝑅 ) ) = ( LSubSp ‘ 𝑆 ) )
28 10 27 eleqtrd ⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ ( LSubSp ‘ 𝑆 ) )