Proof of Theorem ply1ring
Step | Hyp | Ref
| Expression |
1 | | ply1ring.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
2 | | eqid 2738 |
. . . 4
⊢
(PwSer1‘𝑅) = (PwSer1‘𝑅) |
3 | | eqid 2738 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝑃) |
4 | 1, 2, 3 | ply1bas 21366 |
. . 3
⊢
(Base‘𝑃) =
(Base‘(1o mPoly 𝑅)) |
5 | 1, 2, 3 | ply1subrg 21368 |
. . 3
⊢ (𝑅 ∈ Ring →
(Base‘𝑃) ∈
(SubRing‘(PwSer1‘𝑅))) |
6 | 4, 5 | eqeltrrid 2844 |
. 2
⊢ (𝑅 ∈ Ring →
(Base‘(1o mPoly 𝑅)) ∈
(SubRing‘(PwSer1‘𝑅))) |
7 | 1, 2 | ply1val 21365 |
. . 3
⊢ 𝑃 =
((PwSer1‘𝑅) ↾s
(Base‘(1o mPoly 𝑅))) |
8 | 7 | subrgring 20027 |
. 2
⊢
((Base‘(1o mPoly 𝑅)) ∈
(SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring) |
9 | 6, 8 | syl 17 |
1
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |