| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1scltm.k |
|- K = ( Base ` R ) |
| 2 |
|
ply1scltm.p |
|- P = ( Poly1 ` R ) |
| 3 |
|
ply1scltm.x |
|- X = ( var1 ` R ) |
| 4 |
|
ply1scltm.m |
|- .x. = ( .s ` P ) |
| 5 |
|
ply1scltm.n |
|- N = ( mulGrp ` P ) |
| 6 |
|
ply1scltm.e |
|- .^ = ( .g ` N ) |
| 7 |
|
ply1scltm.a |
|- A = ( algSc ` P ) |
| 8 |
2
|
ply1sca2 |
|- ( _I ` R ) = ( Scalar ` P ) |
| 9 |
|
baseid |
|- Base = Slot ( Base ` ndx ) |
| 10 |
9 1
|
strfvi |
|- K = ( Base ` ( _I ` R ) ) |
| 11 |
|
eqid |
|- ( 1r ` P ) = ( 1r ` P ) |
| 12 |
7 8 10 4 11
|
asclval |
|- ( F e. K -> ( A ` F ) = ( F .x. ( 1r ` P ) ) ) |
| 13 |
12
|
adantl |
|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 1r ` P ) ) ) |
| 14 |
|
eqid |
|- ( Base ` P ) = ( Base ` P ) |
| 15 |
3 2 14
|
vr1cl |
|- ( R e. Ring -> X e. ( Base ` P ) ) |
| 16 |
5 14
|
mgpbas |
|- ( Base ` P ) = ( Base ` N ) |
| 17 |
5 11
|
ringidval |
|- ( 1r ` P ) = ( 0g ` N ) |
| 18 |
16 17 6
|
mulg0 |
|- ( X e. ( Base ` P ) -> ( 0 .^ X ) = ( 1r ` P ) ) |
| 19 |
15 18
|
syl |
|- ( R e. Ring -> ( 0 .^ X ) = ( 1r ` P ) ) |
| 20 |
19
|
adantr |
|- ( ( R e. Ring /\ F e. K ) -> ( 0 .^ X ) = ( 1r ` P ) ) |
| 21 |
20
|
oveq2d |
|- ( ( R e. Ring /\ F e. K ) -> ( F .x. ( 0 .^ X ) ) = ( F .x. ( 1r ` P ) ) ) |
| 22 |
13 21
|
eqtr4d |
|- ( ( R e. Ring /\ F e. K ) -> ( A ` F ) = ( F .x. ( 0 .^ X ) ) ) |