Metamath Proof Explorer


Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023)

Ref Expression
Hypotheses mhpvscacl.h
|- H = ( I mHomP R )
mhpvscacl.p
|- P = ( I mPoly R )
mhpvscacl.t
|- .x. = ( .s ` P )
mhpvscacl.k
|- K = ( Base ` R )
mhpvscacl.i
|- ( ph -> I e. V )
mhpvscacl.r
|- ( ph -> R e. Ring )
mhpvscacl.n
|- ( ph -> N e. NN0 )
mhpvscacl.x
|- ( ph -> X e. K )
mhpvscacl.f
|- ( ph -> F e. ( H ` N ) )
Assertion mhpvscacl
|- ( ph -> ( X .x. F ) e. ( H ` N ) )

Proof

Step Hyp Ref Expression
1 mhpvscacl.h
 |-  H = ( I mHomP R )
2 mhpvscacl.p
 |-  P = ( I mPoly R )
3 mhpvscacl.t
 |-  .x. = ( .s ` P )
4 mhpvscacl.k
 |-  K = ( Base ` R )
5 mhpvscacl.i
 |-  ( ph -> I e. V )
6 mhpvscacl.r
 |-  ( ph -> R e. Ring )
7 mhpvscacl.n
 |-  ( ph -> N e. NN0 )
8 mhpvscacl.x
 |-  ( ph -> X e. K )
9 mhpvscacl.f
 |-  ( ph -> F e. ( H ` N ) )
10 eqid
 |-  ( Base ` P ) = ( Base ` P )
11 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
12 eqid
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
13 2 mpllmod
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )
14 5 6 13 syl2anc
 |-  ( ph -> P e. LMod )
15 8 4 eleqtrdi
 |-  ( ph -> X e. ( Base ` R ) )
16 2 5 6 mplsca
 |-  ( ph -> R = ( Scalar ` P ) )
17 16 fveq2d
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
18 15 17 eleqtrd
 |-  ( ph -> X e. ( Base ` ( Scalar ` P ) ) )
19 1 2 10 5 6 7 9 mhpmpl
 |-  ( ph -> F e. ( Base ` P ) )
20 eqid
 |-  ( Scalar ` P ) = ( Scalar ` P )
21 eqid
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
22 10 20 3 21 lmodvscl
 |-  ( ( P e. LMod /\ X e. ( Base ` ( Scalar ` P ) ) /\ F e. ( Base ` P ) ) -> ( X .x. F ) e. ( Base ` P ) )
23 14 18 19 22 syl3anc
 |-  ( ph -> ( X .x. F ) e. ( Base ` P ) )
24 2 4 10 12 23 mplelf
 |-  ( ph -> ( X .x. F ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
25 eqid
 |-  ( .r ` R ) = ( .r ` R )
26 8 adantr
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> X e. K )
27 19 adantr
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> F e. ( Base ` P ) )
28 eldifi
 |-  ( k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
29 28 adantl
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
30 2 3 4 10 25 12 26 27 29 mplvscaval
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( ( X .x. F ) ` k ) = ( X ( .r ` R ) ( F ` k ) ) )
31 2 4 10 12 19 mplelf
 |-  ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
32 ssidd
 |-  ( ph -> ( F supp ( 0g ` R ) ) C_ ( F supp ( 0g ` R ) ) )
33 ovexd
 |-  ( ph -> ( NN0 ^m I ) e. _V )
34 12 33 rabexd
 |-  ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
35 fvexd
 |-  ( ph -> ( 0g ` R ) e. _V )
36 31 32 34 35 suppssr
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( F ` k ) = ( 0g ` R ) )
37 36 oveq2d
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( X ( .r ` R ) ( F ` k ) ) = ( X ( .r ` R ) ( 0g ` R ) ) )
38 4 25 11 ringrz
 |-  ( ( R e. Ring /\ X e. K ) -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
39 6 8 38 syl2anc
 |-  ( ph -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
40 39 adantr
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( X ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
41 30 37 40 3eqtrd
 |-  ( ( ph /\ k e. ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } \ ( F supp ( 0g ` R ) ) ) ) -> ( ( X .x. F ) ` k ) = ( 0g ` R ) )
42 24 41 suppss
 |-  ( ph -> ( ( X .x. F ) supp ( 0g ` R ) ) C_ ( F supp ( 0g ` R ) ) )
43 1 11 12 5 6 7 9 mhpdeg
 |-  ( ph -> ( F supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
44 42 43 sstrd
 |-  ( ph -> ( ( X .x. F ) supp ( 0g ` R ) ) C_ { g e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | ( ( CCfld |`s NN0 ) gsum g ) = N } )
45 1 2 10 11 12 5 6 7 23 44 ismhp2
 |-  ( ph -> ( X .x. F ) e. ( H ` N ) )