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 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 + P y ∈ H ⁡ N
25 24 ralrimiva ⊢ φ ∧ x ∈ H ⁡ N → ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N
26 eqid ⊢ inv g ⁡ P = inv g ⁡ P
27 1 2 26 7 8 9 10 mhpinvcl ⊢ φ ∧ x ∈ H ⁡ N → inv g ⁡ P ⁡ x ∈ H ⁡ N
28 25 27 jca ⊢ φ ∧ x ∈ H ⁡ N → ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
29 28 ralrimiva ⊢ φ → ∀ x ∈ H ⁡ N ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ 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 ⊆ Base P ∧ H ⁡ N ≠ ∅ ∧ ∀ x ∈ H ⁡ N ∀ y ∈ H ⁡ N x + P y ∈ H ⁡ N ∧ inv g ⁡ P ⁡ x ∈ H ⁡ N
33 31 32 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
34 13 17 29 33 mpbir3and ⊢ φ → H ⁡ N ∈ SubGrp ⁡ P