This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mhpvscacl

Description: Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

Ref Expression
Hypotheses mhpvscacl.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
mhpvscacl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mhpvscacl.t ⊢ · = ( ·𝑠 ‘ 𝑃 )
mhpvscacl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mhpvscacl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mhpvscacl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
mhpvscacl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
Assertion mhpvscacl ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( 𝐻 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mhpvscacl.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhpvscacl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhpvscacl.t ⊢ · = ( ·𝑠 ‘ 𝑃 )
4 mhpvscacl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 mhpvscacl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 mhpvscacl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
7 mhpvscacl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐻 ‘ 𝑁 ) )
8 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
9 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 1 7 mhprcl ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
13 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
14 reldmmhp ⊢ Rel dom mHomP
15 14 1 7 elfvov1 ⊢ ( 𝜑 → 𝐼 ∈ V )
16 2 15 5 mpllmodd ⊢ ( 𝜑 → 𝑃 ∈ LMod )
17 6 4 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
18 2 15 5 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
19 18 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
20 17 19 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
21 1 2 8 7 mhpmpl ⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ 𝑃 ) )
22 8 12 3 13 16 20 21 lmodvscld ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
23 2 4 8 10 22 mplelf ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
24 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝑋 ∈ 𝐾 )
26 21 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝐹 ∈ ( Base ‘ 𝑃 ) )
27 eldifi ⊢ ( 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → 𝑘 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
29 2 3 4 8 24 10 25 26 28 mplvscaval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 · 𝐹 ) ‘ 𝑘 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑘 ) ) )
30 2 4 8 10 21 mplelf ⊢ ( 𝜑 → 𝐹 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
31 ssidd ⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) )
32 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
33 30 31 7 32 suppssrg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝐹 ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
34 33 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑘 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
35 4 24 9 5 6 ringrzd ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
37 29 34 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∖ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ) ) → ( ( 𝑋 · 𝐹 ) ‘ 𝑘 ) = ( 0g ‘ 𝑅 ) )
38 23 37 suppss ⊢ ( 𝜑 → ( ( 𝑋 · 𝐹 ) supp ( 0g ‘ 𝑅 ) ) ⊆ ( 𝐹 supp ( 0g ‘ 𝑅 ) ) )
39 1 9 10 7 mhpdeg ⊢ ( 𝜑 → ( 𝐹 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
40 38 39 sstrd ⊢ ( 𝜑 → ( ( 𝑋 · 𝐹 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
41 1 2 8 9 10 11 22 40 ismhp2 ⊢ ( 𝜑 → ( 𝑋 · 𝐹 ) ∈ ( 𝐻 ‘ 𝑁 ) )