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 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 ⊢ Base R = Base R
11 3 adantr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → I ∈ V
12 4 adantr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → R ∈ Ring
13 5 adantr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → N ∈ ℕ 0
14 2 3 4 mplsca ⊢ φ → R = Scalar ⁡ P
15 14 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
16 15 eleq2d ⊢ φ → a ∈ Base R ↔ a ∈ Base Scalar ⁡ P
17 16 biimpar ⊢ φ ∧ a ∈ Base Scalar ⁡ P → a ∈ Base R
18 17 adantrr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ∈ Base R
19 simprr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → b ∈ H ⁡ N
20 1 2 9 10 11 12 13 18 19 mhpvscacl ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ⋅ P b ∈ H ⁡ N
21 20 ralrimivva ⊢ φ → ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ 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 ⊢ 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 ∈ LMod → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
29 23 28 syl ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
30 8 21 29 mpbir2and ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P