Metamath Proof Explorer

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 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
8 1 2 6 7 mhpmpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝑃 ) )
9 8 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝑃 ) ) )
10 9 ssrdv ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) )
11 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
12 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
13 1 11 12 3 4 5 mhp0cl ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 0g ‘ 𝑅 ) } ) ∈ ( 𝐻 ‘ 𝑁 ) )
14 13 ne0d ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ≠ ∅ )
15 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑅 ∈ Grp )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) )
19 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) )
20 1 2 15 17 18 19 mhpaddcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
21 20 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) )
22 eqid ⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
23 1 2 22 16 7 mhpinvcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) )
24 21 23 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ) → ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
25 24 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) )
26 2 mplgrp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
27 3 4 26 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Grp )
28 6 15 22 issubg2 ⊢ ( 𝑃 ∈ Grp → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
29 27 28 syl ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) ↔ ( ( 𝐻 ‘ 𝑁 ) ⊆ ( Base ‘ 𝑃 ) ∧ ( 𝐻 ‘ 𝑁 ) ≠ ∅ ∧ ∀ 𝑥 ∈ ( 𝐻 ‘ 𝑁 ) ( ∀ 𝑦 ∈ ( 𝐻 ‘ 𝑁 ) ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ ( 𝐻 ‘ 𝑁 ) ∧ ( ( invg ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( 𝐻 ‘ 𝑁 ) ) ) ) )
30 10 14 25 29 mpbir3and ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) ∈ ( SubGrp ‘ 𝑃 ) )