| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ply1ring.p |
. . . 4
β’ π = (Poly1βπ
) |
| 2 | | eqid 2733 |
. . . 4
β’
(PwSer1βπ
) = (PwSer1βπ
) |
| 3 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
| 4 | 1, 2, 3 | ply1bas 21719 |
. . 3
β’
(Baseβπ) =
(Baseβ(1o mPoly π
)) |
| 5 | 1, 2, 3 | ply1subrg 21721 |
. . 3
β’ (π
β Ring β
(Baseβπ) β
(SubRingβ(PwSer1βπ
))) |
| 6 | 4, 5 | eqeltrrid 2839 |
. 2
β’ (π
β Ring β
(Baseβ(1o mPoly π
)) β
(SubRingβ(PwSer1βπ
))) |
| 7 | 1, 2 | ply1val 21718 |
. . 3
β’ π =
((PwSer1βπ
) βΎs
(Baseβ(1o mPoly π
))) |
| 8 | 7 | subrgring 20322 |
. 2
β’
((Baseβ(1o mPoly π
)) β
(SubRingβ(PwSer1βπ
)) β π β Ring) |
| 9 | 6, 8 | syl 17 |
1
β’ (π
β Ring β π β Ring) |
