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