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 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
7 4 6 syl 
 |-  ( ph -> R e. Grp )
8 1 2 3 7 5 mhpsubg 
 |-  ( ph -> ( H ` N ) e. ( SubGrp ` P ) )
9 eqid 
 |-  ( .s ` P ) = ( .s ` P )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 3 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> I e. V )
12 4 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> R e. Ring )
13 5 adantr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> N e. NN0 )
14 2 3 4 mplsca 
 |-  ( ph -> R = ( Scalar ` P ) )
15 14 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
16 15 eleq2d 
 |-  ( ph -> ( a e. ( Base ` R ) <-> a e. ( Base ` ( Scalar ` P ) ) ) )
17 16 biimpar 
 |-  ( ( ph /\ a e. ( Base ` ( Scalar ` P ) ) ) -> a e. ( Base ` R ) )
18 17 adantrr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> a e. ( Base ` R ) )
19 simprr 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> b e. ( H ` N ) )
20 1 2 9 10 11 12 13 18 19 mhpvscacl 
 |-  ( ( ph /\ ( a e. ( Base ` ( Scalar ` P ) ) /\ b e. ( H ` N ) ) ) -> ( a ( .s ` P ) b ) e. ( H ` N ) )
21 20 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` ( Scalar ` P ) ) A. b e. ( H ` N ) ( a ( .s ` P ) b ) e. ( H ` N ) )
22 2 mpllmod 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )
23 3 4 22 syl2anc 
 |-  ( ph -> P e. LMod )
24 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
25 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
26 eqid 
 |-  ( Base ` P ) = ( Base ` P )
27 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
28 24 25 26 9 27 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 ) ) ) )
29 23 28 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 ) ) ) )
30 8 21 29 mpbir2and 
 |-  ( ph -> ( H ` N ) e. ( LSubSp ` P ) )