mplvrpmmhm

Description: The action of permuting variables in a multivariate polynomial is a monoid homomorphism. (Contributed by Thierry Arnoux, 11-Jan-2026)

	Ref	Expression
Hypotheses	mplvrpmga.1	$⊢ S = SymGrp (I)$
	mplvrpmga.2	$⊢ P = {Base}_{S}$
	mplvrpmga.3	$⊢ M = {Base}_{(I mPoly R)}$
	mplvrpmga.4	$⊢ A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
	mplvrpmga.5	$⊢ φ \to I \in V$
	mplvrpmmhm.f	$⊢ F = (f \in M ⟼ D A f)$
	mplvrpmmhm.w	$⊢ W = I mPoly R$
	mplvrpmmhm.1	$⊢ φ \to R \in Ring$
	mplvrpmmhm.2	$⊢ φ \to D \in P$
Assertion	mplvrpmmhm	$⊢ φ \to F \in (W MndHom W)$

Proof

Step	Hyp	Ref	Expression
1		mplvrpmga.1	$⊢ S = SymGrp (I)$
2		mplvrpmga.2	$⊢ P = {Base}_{S}$
3		mplvrpmga.3	$⊢ M = {Base}_{(I mPoly R)}$
4		mplvrpmga.4	$⊢ A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
5		mplvrpmga.5	$⊢ φ \to I \in V$
6		mplvrpmmhm.f	$⊢ F = (f \in M ⟼ D A f)$
7		mplvrpmmhm.w	$⊢ W = I mPoly R$
8		mplvrpmmhm.1	$⊢ φ \to R \in Ring$
9		mplvrpmmhm.2	$⊢ φ \to D \in P$
10	7	fveq2i	$⊢ {Base}_{W} = {Base}_{(I mPoly R)}$
11	3 10	eqtr4i	$⊢ M = {Base}_{W}$
12		eqid	$⊢ +_{W} = +_{W}$
13		eqid	$⊢ 0_{W} = 0_{W}$
14	7 5 8	mplringd	$⊢ φ \to W \in Ring$
15	14	ringgrpd	$⊢ φ \to W \in Grp$
16	15	grpmndd	$⊢ φ \to W \in Mnd$
17	1 2 3 4 5	mplvrpmga	$⊢ φ \to A \in (S GrpAct M)$
18	2	gaf	$⊢ A \in (S GrpAct M) \to A : P \times M ⟶ M$
19	17 18	syl	$⊢ φ \to A : P \times M ⟶ M$
20	19	fovcld	$⊢ (φ \land D \in P \land f \in M) \to D A f \in M$
21	20	3expa	$⊢ ((φ \land D \in P) \land f \in M) \to D A f \in M$
22	21	an32s	$⊢ ((φ \land f \in M) \land D \in P) \to D A f \in M$
23	9 22	mpidan	$⊢ (φ \land f \in M) \to D A f \in M$
24	23 6	fmptd	$⊢ φ \to F : M ⟶ M$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
27	26	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
28		simplr	$⊢ ((φ \land i \in M) \land j \in M) \to i \in M$
29	7 25 11 27 28	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to i : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
30	29	adantr	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to i : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
31	30	ffnd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to i Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
32		simpr	$⊢ ((φ \land i \in M) \land j \in M) \to j \in M$
33	7 25 11 27 32	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to j : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
34	33	adantr	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to j : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
35	34	ffnd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to j Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
36		ovex	$⊢ {ℕ_{0}}^{I} \in V$
37	36	rabex	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
38	37	a1i	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
39		breq1	$⊢ h = x \circ D \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((x \circ D)))$
40		nn0ex	$⊢ ℕ_{0} \in V$
41	40	a1i	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
42	5	ad3antrrr	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
43	5	adantr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
44	40	a1i	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
45		breq1	$⊢ h = x \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (x))$
46	45	elrab	$⊢ x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \leftrightarrow (x \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (x))$
47	46	bilani	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (x))$
48	47	simpld	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in ({ℕ_{0}}^{I})$
49	43 44 48	elmaprd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
50	49	ad4ant14	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
51	1 2	symgbasf1o	$⊢ D \in P \to D : I \underset{1-1 onto}{⟶} I$
52	9 51	syl	$⊢ φ \to D : I \underset{1-1 onto}{⟶} I$
53		f1of	$⊢ D : I \underset{1-1 onto}{⟶} I \to D : I ⟶ I$
54	52 53	syl	$⊢ φ \to D : I ⟶ I$
55	54	ad3antrrr	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I ⟶ I$
56	50 55	fcod	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \circ D) : I ⟶ ℕ_{0}$
57	41 42 56	elmapdd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in ({ℕ_{0}}^{I})$
58	47	simprd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (x)$
59	52	adantr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I \underset{1-1 onto}{⟶} I$
60		f1of1	$⊢ D : I \underset{1-1 onto}{⟶} I \to D : I \underset{1-1}{⟶} I$
61	59 60	syl	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I \underset{1-1}{⟶} I$
62		0nn0	$⊢ 0 \in ℕ_{0}$
63	62	a1i	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
64		simpr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
65	58 61 63 64	fsuppco	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((x \circ D))$
66	65	ad4ant14	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((x \circ D))$
67	39 57 66	elrabd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
68		fnfvof	$⊢ ((i Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \land j Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V \land x \circ D \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\})) \to (i {+_{R}}_{f} j) (x \circ D) = i (x \circ D) +_{R} j (x \circ D)$
69	31 35 38 67 68	syl22anc	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (i {+_{R}}_{f} j) (x \circ D) = i (x \circ D) +_{R} j (x \circ D)$
70		oveq2	$⊢ f = i \to D A f = D A i$
71	4	a1i	$⊢ ((φ \land i \in M) \land j \in M) \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
72		simpr	$⊢ (d = D \land f = i) \to f = i$
73		coeq2	$⊢ d = D \to x \circ d = x \circ D$
74	73	adantr	$⊢ (d = D \land f = i) \to x \circ d = x \circ D$
75	72 74	fveq12d	$⊢ (d = D \land f = i) \to f (x \circ d) = i (x \circ D)$
76	75	mpteq2dv	$⊢ (d = D \land f = i) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D))$
77	76	adantl	$⊢ (((φ \land i \in M) \land j \in M) \land (d = D \land f = i)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D))$
78	9	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to D \in P$
79	37	a1i	$⊢ ((φ \land i \in M) \land j \in M) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
80	79	mptexd	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D)) \in V$
81	71 77 78 28 80	ovmpod	$⊢ ((φ \land i \in M) \land j \in M) \to D A i = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D))$
82	70 81	sylan9eqr	$⊢ (((φ \land i \in M) \land j \in M) \land f = i) \to D A f = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D))$
83	6 82 28 80	fvmptd2	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ i (x \circ D))$
84		fvexd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to i (x \circ D) \in V$
85	83 84	fvmpt2d	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to F (i) (x) = i (x \circ D)$
86		oveq2	$⊢ f = j \to D A f = D A j$
87		simpr	$⊢ (d = D \land f = j) \to f = j$
88	73	adantr	$⊢ (d = D \land f = j) \to x \circ d = x \circ D$
89	87 88	fveq12d	$⊢ (d = D \land f = j) \to f (x \circ d) = j (x \circ D)$
90	89	mpteq2dv	$⊢ (d = D \land f = j) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D))$
91	90	adantl	$⊢ (((φ \land i \in M) \land j \in M) \land (d = D \land f = j)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D))$
92	79	mptexd	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D)) \in V$
93	71 91 78 32 92	ovmpod	$⊢ ((φ \land i \in M) \land j \in M) \to D A j = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D))$
94	86 93	sylan9eqr	$⊢ (((φ \land i \in M) \land j \in M) \land f = j) \to D A f = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D))$
95	6 94 32 92	fvmptd2	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ j (x \circ D))$
96		fvexd	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to j (x \circ D) \in V$
97	95 96	fvmpt2d	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to F (j) (x) = j (x \circ D)$
98	85 97	oveq12d	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to F (i) (x) +_{R} F (j) (x) = i (x \circ D) +_{R} j (x \circ D)$
99	69 98	eqtr4d	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (i {+_{R}}_{f} j) (x \circ D) = F (i) (x) +_{R} F (j) (x)$
100	99	mpteq2dva	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i {+_{R}}_{f} j) (x \circ D)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ F (i) (x) +_{R} F (j) (x))$
101	24	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to F : M ⟶ M$
102	101 28	ffvelcdmd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) \in M$
103	7 25 11 27 102	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
104	103	ffnd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
105	101 32	ffvelcdmd	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) \in M$
106	7 25 11 27 105	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
107	106	ffnd	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
108	79 104 107	offvalfv	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) {+_{R}}_{f} F (j) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ F (i) (x) +_{R} F (j) (x))$
109	100 108	eqtr4d	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i {+_{R}}_{f} j) (x \circ D)) = F (i) {+_{R}}_{f} F (j)$
110		oveq2	$⊢ f = i +_{W} j \to D A f = D A (i +_{W} j)$
111		simpr	$⊢ (d = D \land f = i +_{W} j) \to f = i +_{W} j$
112	73	adantr	$⊢ (d = D \land f = i +_{W} j) \to x \circ d = x \circ D$
113	111 112	fveq12d	$⊢ (d = D \land f = i +_{W} j) \to f (x \circ d) = (i +_{W} j) (x \circ D)$
114	113	mpteq2dv	$⊢ (d = D \land f = i +_{W} j) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D))$
115	114	adantl	$⊢ (((φ \land i \in M) \land j \in M) \land (d = D \land f = i +_{W} j)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D))$
116	15	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to W \in Grp$
117	11 12 116 28 32	grpcld	$⊢ ((φ \land i \in M) \land j \in M) \to i +_{W} j \in M$
118	79	mptexd	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D)) \in V$
119	71 115 78 117 118	ovmpod	$⊢ ((φ \land i \in M) \land j \in M) \to D A (i +_{W} j) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D))$
120	110 119	sylan9eqr	$⊢ (((φ \land i \in M) \land j \in M) \land f = i +_{W} j) \to D A f = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D))$
121	6 120 117 118	fvmptd2	$⊢ ((φ \land i \in M) \land j \in M) \to F (i +_{W} j) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D))$
122		eqid	$⊢ +_{R} = +_{R}$
123	7 11 122 12 28 32	mpladd	$⊢ ((φ \land i \in M) \land j \in M) \to i +_{W} j = i {+_{R}}_{f} j$
124	123	fveq1d	$⊢ ((φ \land i \in M) \land j \in M) \to (i +_{W} j) (x \circ D) = (i {+_{R}}_{f} j) (x \circ D)$
125	124	mpteq2dv	$⊢ ((φ \land i \in M) \land j \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i +_{W} j) (x \circ D)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i {+_{R}}_{f} j) (x \circ D))$
126	121 125	eqtrd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i +_{W} j) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (i {+_{R}}_{f} j) (x \circ D))$
127	7 11 122 12 102 105	mpladd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) +_{W} F (j) = F (i) {+_{R}}_{f} F (j)$
128	109 126 127	3eqtr4d	$⊢ ((φ \land i \in M) \land j \in M) \to F (i +_{W} j) = F (i) +_{W} F (j)$
129	128	anasss	$⊢ (φ \land (i \in M \land j \in M)) \to F (i +_{W} j) = F (i) +_{W} F (j)$
130		simpr	$⊢ (φ \land f = 0_{W}) \to f = 0_{W}$
131	130	oveq2d	$⊢ (φ \land f = 0_{W}) \to D A f = D A 0_{W}$
132	4	a1i	$⊢ φ \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
133		simplrr	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f = 0_{W}$
134		eqid	$⊢ 0_{R} = 0_{R}$
135	8	ringgrpd	$⊢ φ \to R \in Grp$
136	7 27 134 13 5 135	mpl0	$⊢ φ \to 0_{W} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}$
137	136	ad2antrr	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0_{W} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}$
138	133 137	eqtrd	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}$
139	73	ad2antrl	$⊢ (φ \land (d = D \land f = 0_{W})) \to x \circ d = x \circ D$
140	139	adantr	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ d = x \circ D$
141	138 140	fveq12d	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f (x \circ d) = (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D)$
142	141	mpteq2dva	$⊢ (φ \land (d = D \land f = 0_{W})) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D))$
143	54	adantr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I ⟶ I$
144	49 143	fcod	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \circ D) : I ⟶ ℕ_{0}$
145	44 43 144	elmapdd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in ({ℕ_{0}}^{I})$
146	39 145 65	elrabd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
147		fvex	$⊢ 0_{R} \in V$
148	147	fvconst2	$⊢ x \circ D \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \to (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D) = 0_{R}$
149	146 148	syl	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D) = 0_{R}$
150	149	mpteq2dva	$⊢ φ \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 0_{R})$
151		fconstmpt	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\} = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 0_{R})$
152	136 151	eqtrdi	$⊢ φ \to 0_{W} = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 0_{R})$
153	150 152	eqtr4d	$⊢ φ \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D)) = 0_{W}$
154	153	adantr	$⊢ (φ \land (d = D \land f = 0_{W})) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ (\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}) (x \circ D)) = 0_{W}$
155	142 154	eqtrd	$⊢ (φ \land (d = D \land f = 0_{W})) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = 0_{W}$
156	11 13	grpidcl	$⊢ W \in Grp \to 0_{W} \in M$
157	15 156	syl	$⊢ φ \to 0_{W} \in M$
158	132 155 9 157 157	ovmpod	$⊢ φ \to D A 0_{W} = 0_{W}$
159	158	adantr	$⊢ (φ \land f = 0_{W}) \to D A 0_{W} = 0_{W}$
160	131 159	eqtrd	$⊢ (φ \land f = 0_{W}) \to D A f = 0_{W}$
161	6 160 157 157	fvmptd2	$⊢ φ \to F (0_{W}) = 0_{W}$
162	11 11 12 12 13 13 16 16 24 129 161	ismhmd	$⊢ φ \to F \in (W MndHom W)$

Metamath Proof Explorer

Theorem mplvrpmmhm

Proof