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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplmapghm.h	$⊢ H = (p \in B ⟼ p (F))$
	mplmapghm.i	$⊢ φ \to I \in V$
	mplmapghm.r	$⊢ φ \to R \in Grp$
	mplmapghm.f	$⊢ φ \to F \in D$
Assertion	mplmapghm	$⊢ φ \to H \in (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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
4		mplmapghm.h	$⊢ H = (p \in B ⟼ p (F))$
5		mplmapghm.i	$⊢ φ \to I \in V$
6		mplmapghm.r	$⊢ φ \to R \in Grp$
7		mplmapghm.f	$⊢ φ \to F \in D$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9		eqid	$⊢ +_{P} = +_{P}$
10		eqid	$⊢ +_{R} = +_{R}$
11	1	mplgrp	$⊢ (I \in V \land R \in Grp) \to P \in Grp$
12	5 6 11	syl2anc	$⊢ φ \to P \in Grp$
13		simpr	$⊢ (φ \land p \in B) \to p \in B$
14	1 8 2 3 13	mplelf	$⊢ (φ \land p \in B) \to p : D ⟶ {Base}_{R}$
15	7	adantr	$⊢ (φ \land p \in B) \to F \in D$
16	14 15	ffvelcdmd	$⊢ (φ \land p \in B) \to p (F) \in {Base}_{R}$
17	16 4	fmptd	$⊢ φ \to H : B ⟶ {Base}_{R}$
18		simprl	$⊢ (φ \land (q \in B \land r \in B)) \to q \in B$
19		simprr	$⊢ (φ \land (q \in B \land r \in B)) \to r \in B$
20	1 2 10 9 18 19	mpladd	$⊢ (φ \land (q \in B \land r \in B)) \to q +_{P} r = q {+_{R}}_{f} r$
21	20	fveq1d	$⊢ (φ \land (q \in B \land r \in B)) \to (q +_{P} r) (F) = (q {+_{R}}_{f} r) (F)$
22	1 8 2 3 18	mplelf	$⊢ (φ \land (q \in B \land r \in B)) \to q : D ⟶ {Base}_{R}$
23	22	ffnd	$⊢ (φ \land (q \in B \land r \in B)) \to q Fn D$
24	1 8 2 3 19	mplelf	$⊢ (φ \land (q \in B \land r \in B)) \to r : D ⟶ {Base}_{R}$
25	24	ffnd	$⊢ (φ \land (q \in B \land r \in B)) \to r Fn D$
26		ovex	$⊢ {ℕ_{0}}^{I} \in V$
27	3 26	rabex2	$⊢ D \in V$
28	27	a1i	$⊢ (φ \land (q \in B \land r \in B)) \to D \in V$
29		inidm	$⊢ D \cap D = D$
30		eqidd	$⊢ ((φ \land (q \in B \land r \in B)) \land F \in D) \to q (F) = q (F)$
31		eqidd	$⊢ ((φ \land (q \in B \land r \in B)) \land F \in D) \to r (F) = r (F)$
32	23 25 28 28 29 30 31	ofval	$⊢ ((φ \land (q \in B \land r \in B)) \land F \in D) \to (q {+_{R}}_{f} r) (F) = q (F) +_{R} r (F)$
33	7 32	mpidan	$⊢ (φ \land (q \in B \land r \in B)) \to (q {+_{R}}_{f} r) (F) = q (F) +_{R} r (F)$
34	21 33	eqtrd	$⊢ (φ \land (q \in B \land r \in B)) \to (q +_{P} r) (F) = q (F) +_{R} r (F)$
35		fveq1	$⊢ p = q +_{P} r \to p (F) = (q +_{P} r) (F)$
36	12	adantr	$⊢ (φ \land (q \in B \land r \in B)) \to P \in Grp$
37	2 9 36 18 19	grpcld	$⊢ (φ \land (q \in B \land r \in B)) \to q +_{P} r \in B$
38		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to (q +_{P} r) (F) \in V$
39	4 35 37 38	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to H (q +_{P} r) = (q +_{P} r) (F)$
40		fveq1	$⊢ p = q \to p (F) = q (F)$
41		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to q (F) \in V$
42	4 40 18 41	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to H (q) = q (F)$
43		fveq1	$⊢ p = r \to p (F) = r (F)$
44		fvexd	$⊢ (φ \land (q \in B \land r \in B)) \to r (F) \in V$
45	4 43 19 44	fvmptd3	$⊢ (φ \land (q \in B \land r \in B)) \to H (r) = r (F)$
46	42 45	oveq12d	$⊢ (φ \land (q \in B \land r \in B)) \to H (q) +_{R} H (r) = q (F) +_{R} r (F)$
47	34 39 46	3eqtr4d	$⊢ (φ \land (q \in B \land r \in B)) \to H (q +_{P} r) = H (q) +_{R} H (r)$
48	2 8 9 10 12 6 17 47	isghmd	$⊢ φ \to H \in (P GrpHom R)$

Metamath Proof Explorer

Theorem mplmapghm

Proof