Description: The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019) (Proof shortened by SN, 3-Jul-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1idvr1.p | ||
ply1idvr1.x | |||
ply1idvr1.n | |||
ply1idvr1.e | |||
Assertion | ply1idvr1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1idvr1.p | ||
2 | ply1idvr1.x | ||
3 | ply1idvr1.n | ||
4 | ply1idvr1.e | ||
5 | eqid | ||
6 | 2 1 5 | vr1cl | |
7 | 3 5 | mgpbas | |
8 | eqid | ||
9 | 3 8 | ringidval | |
10 | 7 9 4 | mulg0 | |
11 | 6 10 | syl |