Description: A homogeneous polynomial defines a homogeneous function; this is mhphf2 with the finite support restriction ( frlmpws , frlmbas ) on the assignments A from variables to values. See comment of mhphf2 . (Contributed by SN, 23-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mhphf3.q | |- Q = ( ( I evalSub S ) ` R ) |
|
mhphf3.h | |- H = ( I mHomP U ) |
||
mhphf3.u | |- U = ( S |`s R ) |
||
mhphf3.k | |- K = ( Base ` S ) |
||
mhphf3.f | |- F = ( S freeLMod I ) |
||
mhphf3.m | |- M = ( Base ` F ) |
||
mhphf3.b | |- .xb = ( .s ` F ) |
||
mhphf3.x | |- .x. = ( .r ` S ) |
||
mhphf3.e | |- .^ = ( .g ` ( mulGrp ` S ) ) |
||
mhphf3.i | |- ( ph -> I e. V ) |
||
mhphf3.s | |- ( ph -> S e. CRing ) |
||
mhphf3.r | |- ( ph -> R e. ( SubRing ` S ) ) |
||
mhphf3.l | |- ( ph -> L e. R ) |
||
mhphf3.n | |- ( ph -> N e. NN0 ) |
||
mhphf3.p | |- ( ph -> X e. ( H ` N ) ) |
||
mhphf3.a | |- ( ph -> A e. M ) |
||
Assertion | mhphf3 | |- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhphf3.q | |- Q = ( ( I evalSub S ) ` R ) |
|
2 | mhphf3.h | |- H = ( I mHomP U ) |
|
3 | mhphf3.u | |- U = ( S |`s R ) |
|
4 | mhphf3.k | |- K = ( Base ` S ) |
|
5 | mhphf3.f | |- F = ( S freeLMod I ) |
|
6 | mhphf3.m | |- M = ( Base ` F ) |
|
7 | mhphf3.b | |- .xb = ( .s ` F ) |
|
8 | mhphf3.x | |- .x. = ( .r ` S ) |
|
9 | mhphf3.e | |- .^ = ( .g ` ( mulGrp ` S ) ) |
|
10 | mhphf3.i | |- ( ph -> I e. V ) |
|
11 | mhphf3.s | |- ( ph -> S e. CRing ) |
|
12 | mhphf3.r | |- ( ph -> R e. ( SubRing ` S ) ) |
|
13 | mhphf3.l | |- ( ph -> L e. R ) |
|
14 | mhphf3.n | |- ( ph -> N e. NN0 ) |
|
15 | mhphf3.p | |- ( ph -> X e. ( H ` N ) ) |
|
16 | mhphf3.a | |- ( ph -> A e. M ) |
|
17 | 4 | subrgss | |- ( R e. ( SubRing ` S ) -> R C_ K ) |
18 | 12 17 | syl | |- ( ph -> R C_ K ) |
19 | 18 13 | sseldd | |- ( ph -> L e. K ) |
20 | 5 6 4 10 19 16 7 8 | frlmvscafval | |- ( ph -> ( L .xb A ) = ( ( I X. { L } ) oF .x. A ) ) |
21 | 20 | fveq2d | |- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) ) |
22 | 5 4 6 | frlmbasmap | |- ( ( I e. V /\ A e. M ) -> A e. ( K ^m I ) ) |
23 | 10 16 22 | syl2anc | |- ( ph -> A e. ( K ^m I ) ) |
24 | 1 2 3 4 8 9 10 11 12 13 14 15 23 | mhphf | |- ( ph -> ( ( Q ` X ) ` ( ( I X. { L } ) oF .x. A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |
25 | 21 24 | eqtrd | |- ( ph -> ( ( Q ` X ) ` ( L .xb A ) ) = ( ( N .^ L ) .x. ( ( Q ` X ) ` A ) ) ) |