| Step |
Hyp |
Ref |
Expression |
| 1 |
|
evls1monply1.1 |
|- Q = ( S evalSub1 R ) |
| 2 |
|
evls1monply1.2 |
|- K = ( Base ` S ) |
| 3 |
|
evls1monply1.3 |
|- W = ( Poly1 ` U ) |
| 4 |
|
evls1monply1.4 |
|- U = ( S |`s R ) |
| 5 |
|
evls1monply1.5 |
|- X = ( var1 ` U ) |
| 6 |
|
evls1monply1.6 |
|- .^ = ( .g ` ( mulGrp ` W ) ) |
| 7 |
|
evls1monply1.7 |
|- ./\ = ( .g ` ( mulGrp ` S ) ) |
| 8 |
|
evls1monply1.8 |
|- .* = ( .s ` W ) |
| 9 |
|
evls1monply1.9 |
|- .x. = ( .r ` S ) |
| 10 |
|
evls1monply1.10 |
|- ( ph -> S e. CRing ) |
| 11 |
|
evls1monply1.11 |
|- ( ph -> R e. ( SubRing ` S ) ) |
| 12 |
|
evls1monply1.12 |
|- ( ph -> A e. R ) |
| 13 |
|
evls1monply1.13 |
|- ( ph -> N e. NN0 ) |
| 14 |
|
evls1monply1.14 |
|- ( ph -> Y e. K ) |
| 15 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
| 16 |
|
eqid |
|- ( mulGrp ` W ) = ( mulGrp ` W ) |
| 17 |
16 15
|
mgpbas |
|- ( Base ` W ) = ( Base ` ( mulGrp ` W ) ) |
| 18 |
4
|
subrgring |
|- ( R e. ( SubRing ` S ) -> U e. Ring ) |
| 19 |
11 18
|
syl |
|- ( ph -> U e. Ring ) |
| 20 |
3
|
ply1ring |
|- ( U e. Ring -> W e. Ring ) |
| 21 |
16
|
ringmgp |
|- ( W e. Ring -> ( mulGrp ` W ) e. Mnd ) |
| 22 |
19 20 21
|
3syl |
|- ( ph -> ( mulGrp ` W ) e. Mnd ) |
| 23 |
5 3 15
|
vr1cl |
|- ( U e. Ring -> X e. ( Base ` W ) ) |
| 24 |
19 23
|
syl |
|- ( ph -> X e. ( Base ` W ) ) |
| 25 |
17 6 22 13 24
|
mulgnn0cld |
|- ( ph -> ( N .^ X ) e. ( Base ` W ) ) |
| 26 |
1 2 3 4 15 8 9 10 11 12 25 14
|
evls1vsca |
|- ( ph -> ( ( Q ` ( A .* ( N .^ X ) ) ) ` Y ) = ( A .x. ( ( Q ` ( N .^ X ) ) ` Y ) ) ) |
| 27 |
1 4 3 5 2 6 7 10 11 13 14
|
evls1varpwval |
|- ( ph -> ( ( Q ` ( N .^ X ) ) ` Y ) = ( N ./\ Y ) ) |
| 28 |
27
|
oveq2d |
|- ( ph -> ( A .x. ( ( Q ` ( N .^ X ) ) ` Y ) ) = ( A .x. ( N ./\ Y ) ) ) |
| 29 |
26 28
|
eqtrd |
|- ( ph -> ( ( Q ` ( A .* ( N .^ X ) ) ) ` Y ) = ( A .x. ( N ./\ Y ) ) ) |