Metamath Proof Explorer

Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

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