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	8	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp )
20	9	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
21		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
22		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
23	1 2 18 19 20 21 22	mhpaddcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
24	23	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
25		eqid	⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
26	1 2 25 8 9 10	mhpinvcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) )
27	24 26	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
28	27	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
29	2	mplgrp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
30	3 4 29	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ Grp )
31	6 18 25	issubg2	⊢ ( 𝑃 ∈ Grp → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
32	30 31	syl	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
33	13 17 28 32	mpbir3and	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )