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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion ply1assa ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 ply1val.1 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
3 eqid ⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
5 1 3 4 ply1subrg ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) )
6 2 5 syl ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) )
7 1 3 4 ply1lss ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) )
8 2 7 syl ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) )
9 3 psr1assa ⊢ ( 𝑅 ∈ CRing → ( PwSer1 ‘ 𝑅 ) ∈ AssAlg )
10 eqid ⊢ ( 1r ‘ ( PwSer1 ‘ 𝑅 ) ) = ( 1r ‘ ( PwSer1 ‘ 𝑅 ) )
11 10 subrg1cl ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) → ( 1r ‘ ( PwSer1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
12 6 11 syl ⊢ ( 𝑅 ∈ CRing → ( 1r ‘ ( PwSer1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
13 eqid ⊢ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) = ( Base ‘ ( PwSer1 ‘ 𝑅 ) )
14 13 subrgss ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
15 6 14 syl ⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) )
16 1 3 ply1val ⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
17 1 4 ply1bas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
18 17 oveq2i ⊢ ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ 𝑃 ) ) = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
19 16 18 eqtr4i ⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
20 eqid ⊢ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) = ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) )
21 19 20 13 10 issubassa ⊢ ( ( ( PwSer1 ‘ 𝑅 ) ∈ AssAlg ∧ ( 1r ‘ ( PwSer1 ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( PwSer1 ‘ 𝑅 ) ) ) → ( 𝑃 ∈ AssAlg ↔ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) ) ) )
22 9 12 15 21 syl3anc ⊢ ( 𝑅 ∈ CRing → ( 𝑃 ∈ AssAlg ↔ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( PwSer1 ‘ 𝑅 ) ) ) ) )
23 6 8 22 mpbir2and ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )