Metamath Proof Explorer

Theorem mplmapghm

Description: The function H mapping polynomials p to their coefficient given a bag of variables F is a group homomorphism. (Contributed by SN, 15-Mar-2025)

Ref Expression
Hypotheses mplmapghm.p 
|- P = ( I mPoly R )
mplmapghm.b 
|- B = ( Base ` P )
mplmapghm.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplmapghm.h 
|- H = ( p e. B |-> ( p ` F ) )
mplmapghm.i 
|- ( ph -> I e. V )
mplmapghm.r 
|- ( ph -> R e. Grp )
mplmapghm.f 
|- ( ph -> F e. D )
Assertion mplmapghm 
|- ( ph -> H e. ( P GrpHom R ) )

Proof

Step Hyp Ref Expression
1 mplmapghm.p 
 |-  P = ( I mPoly R )
2 mplmapghm.b 
 |-  B = ( Base ` P )
3 mplmapghm.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
4 mplmapghm.h 
 |-  H = ( p e. B |-> ( p ` F ) )
5 mplmapghm.i 
 |-  ( ph -> I e. V )
6 mplmapghm.r 
 |-  ( ph -> R e. Grp )
7 mplmapghm.f 
 |-  ( ph -> F e. D )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( +g ` P ) = ( +g ` P )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 1 mplgrp 
 |-  ( ( I e. V /\ R e. Grp ) -> P e. Grp )
12 5 6 11 syl2anc 
 |-  ( ph -> P e. Grp )
13 simpr 
 |-  ( ( ph /\ p e. B ) -> p e. B )
14 1 8 2 3 13 mplelf 
 |-  ( ( ph /\ p e. B ) -> p : D --> ( Base ` R ) )
15 7 adantr 
 |-  ( ( ph /\ p e. B ) -> F e. D )
16 14 15 ffvelcdmd 
 |-  ( ( ph /\ p e. B ) -> ( p ` F ) e. ( Base ` R ) )
17 16 4 fmptd 
 |-  ( ph -> H : B --> ( Base ` R ) )
18 simprl 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> q e. B )
19 simprr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> r e. B )
20 1 2 10 9 18 19 mpladd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q ( +g ` P ) r ) = ( q oF ( +g ` R ) r ) )
21 20 fveq1d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q ( +g ` P ) r ) ` F ) = ( ( q oF ( +g ` R ) r ) ` F ) )
22 1 8 2 3 18 mplelf 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> q : D --> ( Base ` R ) )
23 22 ffnd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> q Fn D )
24 1 8 2 3 19 mplelf 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> r : D --> ( Base ` R ) )
25 24 ffnd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> r Fn D )
26 ovex 
 |-  ( NN0 ^m I ) e. _V
27 3 26 rabex2 
 |-  D e. _V
28 27 a1i 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> D e. _V )
29 inidm 
 |-  ( D i^i D ) = D
30 eqidd 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ F e. D ) -> ( q ` F ) = ( q ` F ) )
31 eqidd 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ F e. D ) -> ( r ` F ) = ( r ` F ) )
32 23 25 28 28 29 30 31 ofval 
 |-  ( ( ( ph /\ ( q e. B /\ r e. B ) ) /\ F e. D ) -> ( ( q oF ( +g ` R ) r ) ` F ) = ( ( q ` F ) ( +g ` R ) ( r ` F ) ) )
33 7 32 mpidan 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q oF ( +g ` R ) r ) ` F ) = ( ( q ` F ) ( +g ` R ) ( r ` F ) ) )
34 21 33 eqtrd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q ( +g ` P ) r ) ` F ) = ( ( q ` F ) ( +g ` R ) ( r ` F ) ) )
35 fveq1 
 |-  ( p = ( q ( +g ` P ) r ) -> ( p ` F ) = ( ( q ( +g ` P ) r ) ` F ) )
36 12 adantr 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> P e. Grp )
37 2 9 36 18 19 grpcld 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q ( +g ` P ) r ) e. B )
38 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( q ( +g ` P ) r ) ` F ) e. _V )
39 4 35 37 38 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( H ` ( q ( +g ` P ) r ) ) = ( ( q ( +g ` P ) r ) ` F ) )
40 fveq1 
 |-  ( p = q -> ( p ` F ) = ( q ` F ) )
41 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( q ` F ) e. _V )
42 4 40 18 41 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( H ` q ) = ( q ` F ) )
43 fveq1 
 |-  ( p = r -> ( p ` F ) = ( r ` F ) )
44 fvexd 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( r ` F ) e. _V )
45 4 43 19 44 fvmptd3 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( H ` r ) = ( r ` F ) )
46 42 45 oveq12d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( ( H ` q ) ( +g ` R ) ( H ` r ) ) = ( ( q ` F ) ( +g ` R ) ( r ` F ) ) )
47 34 39 46 3eqtr4d 
 |-  ( ( ph /\ ( q e. B /\ r e. B ) ) -> ( H ` ( q ( +g ` P ) r ) ) = ( ( H ` q ) ( +g ` R ) ( H ` r ) ) )
48 2 8 9 10 12 6 17 47 isghmd 
 |-  ( ph -> H e. ( P GrpHom R ) )