# Metamath Proof Explorer

## Theorem ply1assa

Description: The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypothesis ply1val.1 $⊢ P = Poly 1 ⁡ R$
Assertion ply1assa $⊢ R ∈ CRing → P ∈ AssAlg$

### Proof

Step Hyp Ref Expression
1 ply1val.1 $⊢ P = Poly 1 ⁡ R$
2 crngring $⊢ R ∈ CRing → R ∈ Ring$
3 eqid $⊢ PwSer 1 ⁡ R = PwSer 1 ⁡ R$
4 eqid $⊢ Base P = Base P$
5 1 3 4 ply1subrg $⊢ R ∈ Ring → Base P ∈ SubRing ⁡ PwSer 1 ⁡ R$
6 2 5 syl $⊢ R ∈ CRing → Base P ∈ SubRing ⁡ PwSer 1 ⁡ R$
7 1 3 4 ply1lss $⊢ R ∈ Ring → Base P ∈ LSubSp ⁡ PwSer 1 ⁡ R$
8 2 7 syl $⊢ R ∈ CRing → Base P ∈ LSubSp ⁡ PwSer 1 ⁡ R$
9 3 psr1assa $⊢ R ∈ CRing → PwSer 1 ⁡ R ∈ AssAlg$
10 eqid $⊢ 1 PwSer 1 ⁡ R = 1 PwSer 1 ⁡ R$
11 10 subrg1cl $⊢ Base P ∈ SubRing ⁡ PwSer 1 ⁡ R → 1 PwSer 1 ⁡ R ∈ Base P$
12 6 11 syl $⊢ R ∈ CRing → 1 PwSer 1 ⁡ R ∈ Base P$
13 eqid $⊢ Base PwSer 1 ⁡ R = Base PwSer 1 ⁡ R$
14 13 subrgss $⊢ Base P ∈ SubRing ⁡ PwSer 1 ⁡ R → Base P ⊆ Base PwSer 1 ⁡ R$
15 6 14 syl $⊢ R ∈ CRing → Base P ⊆ Base PwSer 1 ⁡ R$
16 1 3 ply1val $⊢ P = PwSer 1 ⁡ R ↾ 𝑠 Base 1 𝑜 mPoly R$
17 1 3 4 ply1bas $⊢ Base P = Base 1 𝑜 mPoly R$
18 17 oveq2i $⊢ PwSer 1 ⁡ R ↾ 𝑠 Base P = PwSer 1 ⁡ R ↾ 𝑠 Base 1 𝑜 mPoly R$
19 16 18 eqtr4i $⊢ P = PwSer 1 ⁡ R ↾ 𝑠 Base P$
20 eqid $⊢ LSubSp ⁡ PwSer 1 ⁡ R = LSubSp ⁡ PwSer 1 ⁡ R$
21 19 20 13 10 issubassa $⊢ PwSer 1 ⁡ R ∈ AssAlg ∧ 1 PwSer 1 ⁡ R ∈ Base P ∧ Base P ⊆ Base PwSer 1 ⁡ R → P ∈ AssAlg ↔ Base P ∈ SubRing ⁡ PwSer 1 ⁡ R ∧ Base P ∈ LSubSp ⁡ PwSer 1 ⁡ R$
22 9 12 15 21 syl3anc $⊢ R ∈ CRing → P ∈ AssAlg ↔ Base P ∈ SubRing ⁡ PwSer 1 ⁡ R ∧ Base P ∈ LSubSp ⁡ PwSer 1 ⁡ R$
23 6 8 22 mpbir2and $⊢ R ∈ CRing → P ∈ AssAlg$