Metamath Proof Explorer

Theorem mplassa

Description: The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypothesis mplgrp.p ⊢ P = I mPoly R
Assertion mplassa ⊢ I ∈ V ∧ R ∈ CRing → P ∈ AssAlg

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ P = I mPoly R
2 eqid ⊢ I mPwSer R = I mPwSer R
3 eqid ⊢ Base P = Base P
4 simpl ⊢ I ∈ V ∧ R ∈ CRing → I ∈ V
5 crngring ⊢ R ∈ CRing → R ∈ Ring
6 5 adantl ⊢ I ∈ V ∧ R ∈ CRing → R ∈ Ring
7 2 1 3 4 6 mplsubrg ⊢ I ∈ V ∧ R ∈ CRing → Base P ∈ SubRing ⁡ I mPwSer R
8 2 1 3 4 6 mpllss ⊢ I ∈ V ∧ R ∈ CRing → Base P ∈ LSubSp ⁡ I mPwSer R
9 simpr ⊢ I ∈ V ∧ R ∈ CRing → R ∈ CRing
10 2 4 9 psrassa ⊢ I ∈ V ∧ R ∈ CRing → I mPwSer R ∈ AssAlg
11 eqid ⊢ 1 I mPwSer R = 1 I mPwSer R
12 11 subrg1cl ⊢ Base P ∈ SubRing ⁡ I mPwSer R → 1 I mPwSer R ∈ Base P
13 7 12 syl ⊢ I ∈ V ∧ R ∈ CRing → 1 I mPwSer R ∈ Base P
14 eqid ⊢ Base I mPwSer R = Base I mPwSer R
15 14 subrgss ⊢ Base P ∈ SubRing ⁡ I mPwSer R → Base P ⊆ Base I mPwSer R
16 7 15 syl ⊢ I ∈ V ∧ R ∈ CRing → Base P ⊆ Base I mPwSer R
17 1 2 3 mplval2 ⊢ P = I mPwSer R ↾ 𝑠 Base P
18 eqid ⊢ LSubSp ⁡ I mPwSer R = LSubSp ⁡ I mPwSer R
19 17 18 14 11 issubassa ⊢ I mPwSer R ∈ AssAlg ∧ 1 I mPwSer R ∈ Base P ∧ Base P ⊆ Base I mPwSer R → P ∈ AssAlg ↔ Base P ∈ SubRing ⁡ I mPwSer R ∧ Base P ∈ LSubSp ⁡ I mPwSer R
20 10 13 16 19 syl3anc ⊢ I ∈ V ∧ R ∈ CRing → P ∈ AssAlg ↔ Base P ∈ SubRing ⁡ I mPwSer R ∧ Base P ∈ LSubSp ⁡ I mPwSer R
21 7 8 20 mpbir2and ⊢ I ∈ V ∧ R ∈ CRing → P ∈ AssAlg