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 
|- ( ph -> I e. V )
mhpsubg.r 
|- ( ph -> R e. Grp )
mhpsubg.n 
|- ( ph -> N e. NN0 )
Assertion mhpsubg 
|- ( ph -> ( H ` N ) e. ( SubGrp ` P ) )

Proof

Step Hyp Ref Expression
1 mhpsubg.h 
 |-  H = ( I mHomP R )
2 mhpsubg.p 
 |-  P = ( I mPoly R )
3 mhpsubg.i 
 |-  ( ph -> I e. V )
4 mhpsubg.r 
 |-  ( ph -> R e. Grp )
5 mhpsubg.n 
 |-  ( ph -> N e. NN0 )
6 eqid 
 |-  ( Base ` P ) = ( Base ` P )
7 simpr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> x e. ( H ` N ) )
8 1 2 6 7 mhpmpl 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> x e. ( Base ` P ) )
9 8 ex 
 |-  ( ph -> ( x e. ( H ` N ) -> x e. ( Base ` P ) ) )
10 9 ssrdv 
 |-  ( ph -> ( H ` N ) C_ ( Base ` P ) )
11 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
12 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
13 1 11 12 3 4 5 mhp0cl 
 |-  ( ph -> ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) e. ( H ` N ) )
14 13 ne0d 
 |-  ( ph -> ( H ` N ) =/= (/) )
15 eqid 
 |-  ( +g ` P ) = ( +g ` P )
16 4 adantr 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> R e. Grp )
17 16 adantr 
 |-  ( ( ( ph /\ x e. ( H ` N ) ) /\ y e. ( H ` N ) ) -> R e. Grp )
18 simplr 
 |-  ( ( ( ph /\ x e. ( H ` N ) ) /\ y e. ( H ` N ) ) -> x e. ( H ` N ) )
19 simpr 
 |-  ( ( ( ph /\ x e. ( H ` N ) ) /\ y e. ( H ` N ) ) -> y e. ( H ` N ) )
20 1 2 15 17 18 19 mhpaddcl 
 |-  ( ( ( ph /\ x e. ( H ` N ) ) /\ y e. ( H ` N ) ) -> ( x ( +g ` P ) y ) e. ( H ` N ) )
21 20 ralrimiva 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> A. y e. ( H ` N ) ( x ( +g ` P ) y ) e. ( H ` N ) )
22 eqid 
 |-  ( invg ` P ) = ( invg ` P )
23 1 2 22 16 7 mhpinvcl 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> ( ( invg ` P ) ` x ) e. ( H ` N ) )
24 21 23 jca 
 |-  ( ( ph /\ x e. ( H ` N ) ) -> ( A. y e. ( H ` N ) ( x ( +g ` P ) y ) e. ( H ` N ) /\ ( ( invg ` P ) ` x ) e. ( H ` N ) ) )
25 24 ralrimiva 
 |-  ( ph -> A. x e. ( H ` N ) ( A. y e. ( H ` N ) ( x ( +g ` P ) y ) e. ( H ` N ) /\ ( ( invg ` P ) ` x ) e. ( H ` N ) ) )
26 2 mplgrp 
 |-  ( ( I e. V /\ R e. Grp ) -> P e. Grp )
27 3 4 26 syl2anc 
 |-  ( ph -> P e. Grp )
28 6 15 22 issubg2 
 |-  ( P e. Grp -> ( ( H ` N ) e. ( SubGrp ` P ) <-> ( ( H ` N ) C_ ( Base ` P ) /\ ( H ` N ) =/= (/) /\ A. x e. ( H ` N ) ( A. y e. ( H ` N ) ( x ( +g ` P ) y ) e. ( H ` N ) /\ ( ( invg ` P ) ` x ) e. ( H ` N ) ) ) ) )
29 27 28 syl 
 |-  ( ph -> ( ( H ` N ) e. ( SubGrp ` P ) <-> ( ( H ` N ) C_ ( Base ` P ) /\ ( H ` N ) =/= (/) /\ A. x e. ( H ` N ) ( A. y e. ( H ` N ) ( x ( +g ` P ) y ) e. ( H ` N ) /\ ( ( invg ` P ) ` x ) e. ( H ` N ) ) ) ) )
30 10 14 25 29 mpbir3and 
 |-  ( ph -> ( H ` N ) e. ( SubGrp ` P ) )