Metamath Proof Explorer


Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

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