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

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 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
22 9 21 rabexd ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ ( 𝜑 → 𝑋 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
27 2 23 7 9 16 mplelf ⊢ ( 𝜑 → 𝑌 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
32 1 8 9 6 mhpdeg ⊢ ( 𝜑 → ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
33 31 32 unssd ⊢ ( 𝜑 → ( ( 𝑋 supp ( 0g ‘ 𝑅 ) ) ∪ ( 𝑌 supp ( 0g ‘ 𝑅 ) ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
34 30 33 sstrd ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
35 1 2 7 8 9 10 17 34 ismhp2 ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐻 ‘ 𝑁 ) )