Theorem mhpaddcl

Description: Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023)

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