Metamath Proof Explorer

Theorem mhplss

Description: Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023)

Ref Expression
Hypotheses mhplss.h 
|- H = ( I mHomP R )
mhplss.p 
|- P = ( I mPoly R )
mhplss.i 
|- ( ph -> I e. V )
mhplss.r 
|- ( ph -> R e. Ring )
mhplss.n 
|- ( ph -> N e. NN0 )
Assertion mhplss 
|- ( ph -> ( H ` N ) e. ( LSubSp ` P ) )

Proof

Step Hyp Ref Expression
1 mhplss.h 
 |-  H = ( I mHomP R )
2 mhplss.p 
 |-  P = ( I mPoly R )
3 mhplss.i 
 |-  ( ph -> I e. V )
4 mhplss.r 
 |-  ( ph -> R e. Ring )
5 mhplss.n 
 |-  ( ph -> N e. NN0 )
6 4 ringgrpd 
 |-  ( ph -> R e. Grp )
7 1 2 3 6 5 mhpsubg 
 |-  ( ph -> ( H ` N ) e. ( SubGrp ` P ) )
8 eqid 
 |-  ( .s ` P ) = ( .s ` P )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 4 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> R e. Ring )
11 5 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> N e. NN0 )
12 2 3 4 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
13 12 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
14 13 eqimsscd 
 |-  ( ph -> ( Base ` ( Scalar ` P ) ) C_ ( Base ` R ) )
15 14 sselda 
 |-  ( ( ph /\ a e. ( Base ` ( Scalar ` P ) ) ) -> a e. ( Base ` R ) )
16 15 adantrr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> a e. ( Base ` R ) )
17 simprr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> b e. ( H ` N ) )
18 1 2 8 9 10 11 16 17 mhpvscacl 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> ( a ( .s ` P ) b ) e. ( H ` N ) )
19 18 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` P ) ) A. b e. ( H ` N ) ( a ( .s ` P ) b ) e. ( H ` N ) )
20 2 mpllmod 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )
21 3 4 20 syl2anc 
 |-  ( ph -> P e. LMod )
22 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
23 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
24 eqid 
 |-  ( Base ` P ) = ( Base ` P )
25 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
26 22 23 24 8 25 islss4 
 |-  ( P e. LMod -> ( ( H ` N ) e. ( LSubSp ` P ) <-> ( ( H ` N ) e. ( SubGrp ` P ) /\ A. a e. ( Base ` ( Scalar ` P ) ) A. b e. ( H ` N ) ( a ( .s ` P ) b ) e. ( H ` N ) ) ) )
27 21 26 syl 
 |-  ( ph -> ( ( H ` N ) e. ( LSubSp ` P ) <-> ( ( H ` N ) e. ( SubGrp ` P ) /\ A. a e. ( Base ` ( Scalar ` P ) ) A. b e. ( H ` N ) ( a ( .s ` P ) b ) e. ( H ` N ) ) ) )
28 7 19 27 mpbir2and 
 |-  ( ph -> ( H ` N ) e. ( LSubSp ` P ) )