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 ) )

Metamath Proof Explorer

Theorem mplmapghm

Proof