Metamath Proof Explorer


Theorem mhphf3

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

Proof

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