Description: The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mplgrp.p | ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) | |
Assertion | mplgrp | ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp ) |
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 ) |