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=ImHomPR
mhplss.p ⊢P=ImPolyR
mhplss.i ⊢φ→I∈V
mhplss.r ⊢φ→R∈Ring
mhplss.n ⊢φ→N∈ℕ0
Assertion mhplss ⊢φ→H⁡N∈LSubSp⁡P

Proof

Step Hyp Ref Expression
1 mhplss.h ⊢H=ImHomPR
2 mhplss.p ⊢P=ImPolyR
3 mhplss.i ⊢φ→I∈V
4 mhplss.r ⊢φ→R∈Ring
5 mhplss.n ⊢φ→N∈ℕ0
6 ringgrp ⊢R∈Ring→R∈Grp
7 4 6 syl ⊢φ→R∈Grp
8 1 2 3 7 5 mhpsubg ⊢φ→H⁡N∈SubGrp⁡P
9 eqid ⊢⋅P=⋅P
10 eqid ⊢BaseR=BaseR
11 3 adantr ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→I∈V
12 4 adantr ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→R∈Ring
13 5 adantr ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→N∈ℕ0
14 2 3 4 mplsca ⊢φ→R=Scalar⁡P
15 14 fveq2d ⊢φ→BaseR=BaseScalar⁡P
16 15 eleq2d ⊢φ→a∈BaseR↔a∈BaseScalar⁡P
17 16 biimpar ⊢φ∧a∈BaseScalar⁡P→a∈BaseR
18 17 adantrr ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→a∈BaseR
19 simprr ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→b∈H⁡N
20 1 2 9 10 11 12 13 18 19 mhpvscacl ⊢φ∧a∈BaseScalar⁡P∧b∈H⁡N→a⋅Pb∈H⁡N
21 20 ralrimivva ⊢φ→∀a∈BaseScalar⁡P∀b∈H⁡Na⋅Pb∈H⁡N
22 2 mpllmod ⊢I∈V∧R∈Ring→P∈LMod
23 3 4 22 syl2anc ⊢φ→P∈LMod
24 eqid ⊢Scalar⁡P=Scalar⁡P
25 eqid ⊢BaseScalar⁡P=BaseScalar⁡P
26 eqid ⊢BaseP=BaseP
27 eqid ⊢LSubSp⁡P=LSubSp⁡P
28 24 25 26 9 27 islss4 ⊢P∈LMod→H⁡N∈LSubSp⁡P↔H⁡N∈SubGrp⁡P∧∀a∈BaseScalar⁡P∀b∈H⁡Na⋅Pb∈H⁡N
29 23 28 syl ⊢φ→H⁡N∈LSubSp⁡P↔H⁡N∈SubGrp⁡P∧∀a∈BaseScalar⁡P∀b∈H⁡Na⋅Pb∈H⁡N
30 8 21 29 mpbir2and ⊢φ→H⁡N∈LSubSp⁡P