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 ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
mhplss.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mhplss.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mhplss.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mhplss.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion mhplss ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 mhplss.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhplss.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhplss.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 mhplss.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 mhplss.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 4 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
7 1 2 3 6 5 mhpsubg ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )
8 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
11 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
12 2 3 4 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
13 12 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
14 13 eqimsscd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⊆ ( Base ‘ 𝑅 ) )
15 14 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
16 15 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
17 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) )
18 1 2 8 9 10 11 16 17 mhpvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
19 18 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
20 2 mpllmod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
21 3 4 20 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ LMod )
22 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
23 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
24 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
25 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
26 22 23 24 8 25 islss4 ⊢ ( 𝑃 ∈ LMod → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
27 21 26 syl ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
28 7 19 27 mpbir2and ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) )