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 = I mHomP R
mhpsubg.p ⊢ P = I mPoly R
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 = I mHomP R
2 mhpsubg.p ⊢ P = I mPoly R
3 mhpsubg.i ⊢ φ → I ∈ V
4 mhpsubg.r ⊢ φ → R ∈ Grp
5 mhpsubg.n ⊢ φ → N ∈ ℕ 0
6 eqid ⊢ Base P = Base P
7 simpr ⊢ φ ∧ x ∈ H ⁡ N → x ∈ H ⁡ N
8 1 2 6 7 mhpmpl ⊢ φ ∧ x ∈ H ⁡ N → x ∈ Base P
9 8 ex ⊢ φ → x ∈ H ⁡ N → x ∈ Base P
10 9 ssrdv ⊢ φ → H ⁡ N ⊆ Base P
11 eqid ⊢ 0 R = 0 R
12 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
13 1 11 12 3 4 5 mhp0cl ⊢ φ → h ∈ ℕ 0 I | h -1 ℕ ∈ Fin × 0 R ∈ H ⁡ N
14 13 ne0d ⊢ φ → H ⁡ N ≠ ∅
15 eqid ⊢ + P = + P
16 4 adantr ⊢ φ ∧ x ∈ H ⁡ N → R ∈ Grp
17 16 adantr ⊢ φ ∧ x ∈ H ⁡ N ∧ y ∈ H ⁡ N → R ∈ Grp
18 simplr ⊢ φ ∧ x ∈ H ⁡ N ∧ y ∈ H ⁡ N → x ∈ H ⁡ N
19 simpr ⊢ φ ∧ x ∈ H ⁡ N ∧ y ∈ H ⁡ N → y ∈ H ⁡ N
20 1 2 15 17 18 19 mhpaddcl ⊢ φ ∧ x ∈ H ⁡ N ∧ y ∈ H ⁡ N → x + P y ∈ H ⁡ N
21 20 ralrimiva ⊢ φ ∧ x ∈ H ⁡ N → ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N
22 eqid ⊢ inv g ⁡ P = inv g ⁡ P
23 1 2 22 16 7 mhpinvcl ⊢ φ ∧ x ∈ H ⁡ N → inv g ⁡ P ⁡ x ∈ H ⁡ N
24 21 23 jca ⊢ φ ∧ x ∈ H ⁡ N → ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
25 24 ralrimiva ⊢ φ → ∀ x ∈ H ⁡ N ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
26 2 mplgrp ⊢ I ∈ V ∧ R ∈ Grp → P ∈ Grp
27 3 4 26 syl2anc ⊢ φ → P ∈ Grp
28 6 15 22 issubg2 ⊢ P ∈ Grp → H ⁡ N ∈ SubGrp ⁡ P ↔ H ⁡ N ⊆ Base P ∧ H ⁡ N ≠ ∅ ∧ ∀ x ∈ H ⁡ N ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
29 27 28 syl ⊢ φ → H ⁡ N ∈ SubGrp ⁡ P ↔ H ⁡ N ⊆ Base P ∧ H ⁡ N ≠ ∅ ∧ ∀ x ∈ H ⁡ N ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
30 10 14 25 29 mpbir3and ⊢ φ → H ⁡ N ∈ SubGrp ⁡ P