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 3 4 mpllmodd ⊢ φ → P ∈ LMod
21 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
22 eqid ⊢ Base Scalar ⁡ P = Base Scalar ⁡ P
23 eqid ⊢ Base P = Base P
24 eqid ⊢ LSubSp ⁡ P = LSubSp ⁡ P
25 21 22 23 8 24 islss4 ⊢ P ∈ LMod → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
26 20 25 syl ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
27 7 19 26 mpbir2and ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P