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 ⊢H=ImHomPR
mhpsubg.p ⊢P=ImPolyR
mhpsubg.i ⊢φ→I∈V
mhpsubg.r ⊢φ→R∈Grp
mhpsubg.n ⊢φ→N∈ℕ0
Assertion mhpsubg ⊢φ→H⁡N∈SubGrp⁡P

Proof

Step Hyp Ref Expression
1 mhpsubg.h ⊢H=ImHomPR
2 mhpsubg.p ⊢P=ImPolyR
3 mhpsubg.i ⊢φ→I∈V
4 mhpsubg.r ⊢φ→R∈Grp
5 mhpsubg.n ⊢φ→N∈ℕ0
6 eqid ⊢BaseP=BaseP
7 3 adantr ⊢φ∧x∈H⁡N→I∈V
8 4 adantr ⊢φ∧x∈H⁡N→R∈Grp
9 5 adantr ⊢φ∧x∈H⁡N→N∈ℕ0
10 simpr ⊢φ∧x∈H⁡N→x∈H⁡N
11 1 2 6 7 8 9 10 mhpmpl ⊢φ∧x∈H⁡N→x∈BaseP
12 11 ex ⊢φ→x∈H⁡N→x∈BaseP
13 12 ssrdv ⊢φ→H⁡N⊆BaseP
14 eqid ⊢0R=0R
15 eqid ⊢h∈ℕ0I|h-1ℕ∈Fin=h∈ℕ0I|h-1ℕ∈Fin
16 1 14 15 3 4 5 mhp0cl ⊢φ→h∈ℕ0I|h-1ℕ∈Fin×0R∈H⁡N
17 16 ne0d ⊢φ→H⁡N≠∅
18 eqid ⊢+P=+P
19 7 adantr ⊢φ∧x∈H⁡N∧y∈H⁡N→I∈V
20 8 adantr ⊢φ∧x∈H⁡N∧y∈H⁡N→R∈Grp
21 9 adantr ⊢φ∧x∈H⁡N∧y∈H⁡N→N∈ℕ0
22 simplr ⊢φ∧x∈H⁡N∧y∈H⁡N→x∈H⁡N
23 simpr ⊢φ∧x∈H⁡N∧y∈H⁡N→y∈H⁡N
24 1 2 18 19 20 21 22 23 mhpaddcl ⊢φ∧x∈H⁡N∧y∈H⁡N→x+Py∈H⁡N
25 24 ralrimiva ⊢φ∧x∈H⁡N→∀y∈H⁡Nx+Py∈H⁡N
26 eqid ⊢invg⁡P=invg⁡P
27 1 2 26 7 8 9 10 mhpinvcl ⊢φ∧x∈H⁡N→invg⁡P⁡x∈H⁡N
28 25 27 jca ⊢φ∧x∈H⁡N→∀y∈H⁡Nx+Py∈H⁡N∧invg⁡P⁡x∈H⁡N
29 28 ralrimiva ⊢φ→∀x∈H⁡N∀y∈H⁡Nx+Py∈H⁡N∧invg⁡P⁡x∈H⁡N
30 2 mplgrp ⊢I∈V∧R∈Grp→P∈Grp
31 3 4 30 syl2anc ⊢φ→P∈Grp
32 6 18 26 issubg2 ⊢P∈Grp→H⁡N∈SubGrp⁡P↔H⁡N⊆BaseP∧H⁡N≠∅∧∀x∈H⁡N∀y∈H⁡Nx+Py∈H⁡N∧invg⁡P⁡x∈H⁡N
33 31 32 syl ⊢φ→H⁡N∈SubGrp⁡P↔H⁡N⊆BaseP∧H⁡N≠∅∧∀x∈H⁡N∀y∈H⁡Nx+Py∈H⁡N∧invg⁡P⁡x∈H⁡N
34 13 17 29 33 mpbir3and ⊢φ→H⁡N∈SubGrp⁡P