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 | |- P = ( Poly1 ` R ) |
|
| ply1idvr1.x | |- X = ( var1 ` R ) |
||
| ply1idvr1.n | |- N = ( mulGrp ` P ) |
||
| ply1idvr1.e | |- .^ = ( .g ` N ) |
||
| Assertion | ply1idvr1 | |- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ply1idvr1.p | |- P = ( Poly1 ` R ) |
|
| 2 | ply1idvr1.x | |- X = ( var1 ` R ) |
|
| 3 | ply1idvr1.n | |- N = ( mulGrp ` P ) |
|
| 4 | ply1idvr1.e | |- .^ = ( .g ` N ) |
|
| 5 | eqid | |- ( Base ` P ) = ( Base ` P ) |
|
| 6 | 2 1 5 | vr1cl | |- ( R e. Ring -> X e. ( Base ` P ) ) |
| 7 | 3 5 | mgpbas | |- ( Base ` P ) = ( Base ` N ) |
| 8 | eqid | |- ( 1r ` P ) = ( 1r ` P ) |
|
| 9 | 3 8 | ringidval | |- ( 1r ` P ) = ( 0g ` N ) |
| 10 | 7 9 4 | mulg0 | |- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) ) |
| 11 | 6 10 | syl | |- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) ) |