Theorem mhpsubg

Description: Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023)

	Ref	Expression
Hypotheses	mhpsubg.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhpsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhpsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhpsubg.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	mhpsubg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	mhpsubg	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		mhpsubg.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhpsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mhpsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4		mhpsubg.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
5		mhpsubg.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝐼 ∈ 𝑉 )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
11	1 2 6 7 8 9 10	mhpmpl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
12	11	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) ) )
13	12	ssrdv	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) )
14		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
15		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
16	1 14 15 3 4 5	mhp0cl	⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ∈ ( 𝐻 ‘ 𝑁 ) )
17	16	ne0d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ≠ ∅ )
18		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
19	7	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝐼 ∈ 𝑉 )
20	8	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp )
21	9	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
22		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
23		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
24	1 2 18 19 20 21 22 23	mhpaddcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
25	24	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
26		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
27	1 2 26 7 8 9 10	mhpinvcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) )
28	25 27	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
29	28	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
30	2	mplgrp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
31	3 4 30	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ Grp )
32	6 18 26	issubg2	⊢ ( 𝑃 ∈ Grp → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
33	31 32	syl	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
34	13 17 29 33	mpbir3and	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )