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 2 3 4 mplsca ⊢ φ → R = Scalar ⁡ P
12 11 fveq2d ⊢ φ → Base R = Base Scalar ⁡ P
13 12 eqimsscd ⊢ φ → Base Scalar ⁡ P ⊆ Base R
14 13 sselda ⊢ φ ∧ a ∈ Base Scalar ⁡ P → a ∈ Base R
15 14 adantrr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ∈ Base R
16 simprr ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → b ∈ H ⁡ N
17 1 2 8 9 10 15 16 mhpvscacl ⊢ φ ∧ a ∈ Base Scalar ⁡ P ∧ b ∈ H ⁡ N → a ⋅ P b ∈ H ⁡ N
18 17 ralrimivva ⊢ φ → ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
19 2 3 4 mpllmodd ⊢ φ → P ∈ LMod
20 eqid ⊢ Scalar ⁡ P = Scalar ⁡ P
21 eqid ⊢ Base Scalar ⁡ P = Base Scalar ⁡ P
22 eqid ⊢ Base P = Base P
23 eqid ⊢ LSubSp ⁡ P = LSubSp ⁡ P
24 20 21 22 8 23 islss4 ⊢ P ∈ LMod → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
25 19 24 syl ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P ↔ H ⁡ N ∈ SubGrp ⁡ P ∧ ∀ a ∈ Base Scalar ⁡ P ∀ b ∈ H ⁡ N a ⋅ P b ∈ H ⁡ N
26 7 18 25 mpbir2and ⊢ φ → H ⁡ N ∈ LSubSp ⁡ P