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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion mplassa ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
4 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝐼 ∈ 𝑉 )
5 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
6 5 adantl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
7 2 1 3 4 6 mplsubrg ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
8 2 1 3 4 6 mpllss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
9 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
10 2 4 9 psrassa ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg )
11 eqid ⊢ ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) )
12 11 subrg1cl ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
13 7 12 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) )
14 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
15 14 subrgss ⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
16 7 15 syl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
17 1 2 3 mplval2 ⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
18 eqid ⊢ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) )
19 17 18 14 11 issubassa ⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg ∧ ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ ( Base ‘ 𝑃 ) ∧ ( Base ‘ 𝑃 ) ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑃 ∈ AssAlg ↔ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) )
20 10 13 16 19 syl3anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → ( 𝑃 ∈ AssAlg ↔ ( ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) )
21 7 8 20 mpbir2and ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ CRing ) → 𝑃 ∈ AssAlg )