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