Metamath Proof Explorer


Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

Ref Expression
Hypotheses mhpaddcl.h 𝐻 = ( 𝐼 mHomP 𝑅 )
mhpaddcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mhpaddcl.a + = ( +g𝑃 )
mhpaddcl.r ( 𝜑𝑅 ∈ Grp )
mhpaddcl.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
mhpaddcl.y ( 𝜑𝑌 ∈ ( 𝐻𝑁 ) )
Assertion mhpaddcl ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐻𝑁 ) )

Proof

Step Hyp Ref Expression
1 mhpaddcl.h 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhpaddcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhpaddcl.a + = ( +g𝑃 )
4 mhpaddcl.r ( 𝜑𝑅 ∈ Grp )
5 mhpaddcl.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
6 mhpaddcl.y ( 𝜑𝑌 ∈ ( 𝐻𝑁 ) )
7 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 eqid ( 0g𝑅 ) = ( 0g𝑅 )
9 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
10 1 5 mhprcl ( 𝜑𝑁 ∈ ℕ0 )
11 reldmmhp Rel dom mHomP
12 11 1 5 elfvov1 ( 𝜑𝐼 ∈ V )
13 2 mplgrp ( ( 𝐼 ∈ V ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
14 12 4 13 syl2anc ( 𝜑𝑃 ∈ Grp )
15 1 2 7 5 mhpmpl ( 𝜑𝑋 ∈ ( Base ‘ 𝑃 ) )
16 1 2 7 6 mhpmpl ( 𝜑𝑌 ∈ ( Base ‘ 𝑃 ) )
17 7 3 14 15 16 grpcld ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( Base ‘ 𝑃 ) )
18 eqid ( +g𝑅 ) = ( +g𝑅 )
19 2 7 18 3 15 16 mpladd ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑋f ( +g𝑅 ) 𝑌 ) )
20 19 oveq1d ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g𝑅 ) ) = ( ( 𝑋f ( +g𝑅 ) 𝑌 ) supp ( 0g𝑅 ) ) )
21 ovexd ( 𝜑 → ( ℕ0m 𝐼 ) ∈ V )
22 9 21 rabexd ( 𝜑 → { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V )
23 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
24 23 8 grpidcl ( 𝑅 ∈ Grp → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
25 4 24 syl ( 𝜑 → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
26 2 23 7 9 15 mplelf ( 𝜑𝑋 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
27 2 23 7 9 16 mplelf ( 𝜑𝑌 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
28 23 18 8 4 25 grplidd ( 𝜑 → ( ( 0g𝑅 ) ( +g𝑅 ) ( 0g𝑅 ) ) = ( 0g𝑅 ) )
29 22 25 26 27 28 suppofssd ( 𝜑 → ( ( 𝑋f ( +g𝑅 ) 𝑌 ) supp ( 0g𝑅 ) ) ⊆ ( ( 𝑋 supp ( 0g𝑅 ) ) ∪ ( 𝑌 supp ( 0g𝑅 ) ) ) )
30 20 29 eqsstrd ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g𝑅 ) ) ⊆ ( ( 𝑋 supp ( 0g𝑅 ) ) ∪ ( 𝑌 supp ( 0g𝑅 ) ) ) )
31 1 8 9 5 mhpdeg ( 𝜑 → ( 𝑋 supp ( 0g𝑅 ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
32 1 8 9 6 mhpdeg ( 𝜑 → ( 𝑌 supp ( 0g𝑅 ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
33 31 32 unssd ( 𝜑 → ( ( 𝑋 supp ( 0g𝑅 ) ) ∪ ( 𝑌 supp ( 0g𝑅 ) ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
34 30 33 sstrd ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g𝑅 ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
35 1 2 7 8 9 10 17 34 ismhp2 ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐻𝑁 ) )