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 2 3 4 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
12 11 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
13 12 eqimsscd ⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝑃 ) ) ⊆ ( Base ‘ 𝑅 ) )
14 13 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
15 14 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) )
17 1 2 8 9 10 15 16 mhpvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
18 17 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
19 2 3 4 mpllmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
20 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
21 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
22 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
23 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
24 20 21 22 8 23 islss4 ⊢ ( 𝑃 ∈ LMod → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
25 19 24 syl ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
26 7 18 25 mpbir2and ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) )