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 ) ) |