Theorem mplgrp

Description: The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015)

	Ref	Expression
Hypothesis	mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion	mplgrp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		mplgrp.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
4		simpl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝐼 ∈ 𝑉 )
5		simpr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑅 ∈ Grp )
6	2 1 3 4 5	mplsubg	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
7	1 2 3	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
8	7	subggrp	⊢ ( ( Base ‘ 𝑃 ) ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) → 𝑃 ∈ Grp )
9	6 8	syl	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )