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 2 3 4 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
12 11 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
13 12 eqimsscd 
 |-  ( ph -> ( Base ` ( Scalar ` P ) ) C_ ( Base ` R ) )
14 13 sselda 
 |-  ( ( ph /\ a e. ( Base ` ( Scalar ` P ) ) ) -> a e. ( Base ` R ) )
15 14 adantrr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> a e. ( Base ` R ) )
16 simprr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> b e. ( H ` N ) )
17 1 2 8 9 10 15 16 mhpvscacl 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> ( a ( .s ` P ) b ) e. ( H ` N ) )
18 17 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` P ) ) A. b e. ( H ` N ) ( a ( .s ` P ) b ) e. ( H ` N ) )
19 2 3 4 mpllmodd 
 |-  ( ph -> P e. LMod )
20 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
21 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
22 eqid 
 |-  ( Base ` P ) = ( Base ` P )
23 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
24 20 21 22 8 23 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 ) ) ) )
25 19 24 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 ) ) ) )
26 7 18 25 mpbir2and 
 |-  ( ph -> ( H ` N ) e. ( LSubSp ` P ) )