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 ⊢ φ → 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 = I mHomP R
2 mhplss.p ⊢ P = I mPoly R
3 mhplss.i ⊢ φ → I ∈ V
4 mhplss.r ⊢ φ → R ∈ Ring
5 mhplss.n ⊢ φ → N ∈ ℕ 0
6 4 ringgrpd ⊢ φ → R ∈ Grp
7 1 2 3 6 5 mhpsubg ⊢ φ → H ⁡ N ∈ SubGrp ⁡ P
8 eqid ⊢ ⋅ P = ⋅ P
9 eqid ⊢ Base R = Base R
10 4 adantr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → R ∈ Ring
11 5 adantr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → N ∈ ℕ 0
12 2 3 4 mplsca ⊢ φ → R = Scalar ⁡ P
13 12 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
14 13 eqimsscd ⊢ φ → Base Scalar ⁡ P ⊆ Base R
15 14 sselda ⊢ φ ∧ a ∈ Base Scalar ⁡ P → a ∈ Base R
16 15 adantrr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ∈ Base R
17 simprr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → b ∈ H ⁡ N
18 1 2 8 9 10 11 16 17 mhpvscacl ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ⋅ P b ∈ H ⁡ N
19 18 ralrimivva ⊢ φ → ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
20 2 mpllmod ⊢ I ∈ V ∧ R ∈ Ring → P ∈ LMod
21 3 4 20 syl2anc ⊢ φ → P ∈ 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 ∈ LMod → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
27 21 26 syl ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
28 7 19 27 mpbir2and ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P