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 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7 4 6 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
8 1 2 3 7 5 mhpsubg ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )
9 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝐼 ∈ 𝑉 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑅 ∈ Ring )
13 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
14 2 3 4 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
15 14 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
16 15 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
17 16 biimpar ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
18 17 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) )
20 1 2 9 10 11 12 13 18 19 mhpvscacl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ) ) → ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
21 20 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) )
22 2 mpllmod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
23 3 4 22 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ LMod )
24 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
25 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
26 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
27 eqid ⊢ ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 )
28 24 25 26 9 27 islss4 ⊢ ( 𝑃 ∈ LMod → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
29 23 28 syl ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ∧ ∀ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∀ 𝑏 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑎 ( ·𝑠 ‘ 𝑃 ) 𝑏 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) )
30 8 21 29 mpbir2and ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( LSubSp ‘ 𝑃 ) )