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 ` R ) = ( Base ` R ) |
6 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
7 |
5 6
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) ) |
8 |
|
eqid |
|- ( .s ` P ) = ( .s ` P ) |
9 |
|
eqid |
|- ( algSc ` P ) = ( algSc ` P ) |
10 |
5 1 2 8 3 4 9
|
ply1scltm |
|- ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) ) |
11 |
7 10
|
mpdan |
|- ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) ) |
12 |
1
|
ply1sca |
|- ( R e. Ring -> R = ( Scalar ` P ) ) |
13 |
12
|
fveq2d |
|- ( R e. Ring -> ( 1r ` R ) = ( 1r ` ( Scalar ` P ) ) ) |
14 |
13
|
oveq1d |
|- ( R e. Ring -> ( ( 1r ` R ) ( .s ` P ) ( 0 .^ X ) ) = ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) ) |
15 |
1
|
ply1lmod |
|- ( R e. Ring -> P e. LMod ) |
16 |
|
0nn0 |
|- 0 e. NN0 |
17 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
18 |
1 2 3 4 17
|
ply1moncl |
|- ( ( R e. Ring /\ 0 e. NN0 ) -> ( 0 .^ X ) e. ( Base ` P ) ) |
19 |
16 18
|
mpan2 |
|- ( R e. Ring -> ( 0 .^ X ) e. ( Base ` P ) ) |
20 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
21 |
|
eqid |
|- ( 1r ` ( Scalar ` P ) ) = ( 1r ` ( Scalar ` P ) ) |
22 |
17 20 8 21
|
lmodvs1 |
|- ( ( P e. LMod /\ ( 0 .^ X ) e. ( Base ` P ) ) -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) = ( 0 .^ X ) ) |
23 |
15 19 22
|
syl2anc |
|- ( R e. Ring -> ( ( 1r ` ( Scalar ` P ) ) ( .s ` P ) ( 0 .^ X ) ) = ( 0 .^ X ) ) |
24 |
11 14 23
|
3eqtrrd |
|- ( R e. Ring -> ( 0 .^ X ) = ( ( algSc ` P ) ` ( 1r ` R ) ) ) |
25 |
|
eqid |
|- ( 1r ` P ) = ( 1r ` P ) |
26 |
1 9 6 25
|
ply1scl1 |
|- ( R e. Ring -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) ) |
27 |
24 26
|
eqtrd |
|- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) ) |