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	biimpi	$⊢ x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \to (x \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (x))$
48	47	adantl	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (x))$
49	48	simpld	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in ({ℕ_{0}}^{I})$
50	43 44 49	elmaprd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
51	50	ad4ant14	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
52	1 2	symgbasf1o	$⊢ D \in P \to D : I \underset{1-1 onto}{⟶} I$
53	9 52	syl	$⊢ φ \to D : I \underset{1-1 onto}{⟶} I$
54		f1of	$⊢ D : I \underset{1-1 onto}{⟶} I \to D : I ⟶ I$
55	53 54	syl	$⊢ φ \to D : I ⟶ I$
56	55	ad3antrrr	$⊢ (((φ \land i \in M) \land j \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I ⟶ I$
57	51 56	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}$
58	41 42 57	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})$
59	48	simprd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (x)$
60	53	adantr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I \underset{1-1 onto}{⟶} I$
61		f1of1	$⊢ D : I \underset{1-1 onto}{⟶} I \to D : I \underset{1-1}{⟶} I$
62	60 61	syl	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I \underset{1-1}{⟶} I$
63		0nn0	$⊢ 0 \in ℕ_{0}$
64	63	a1i	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
65		simpr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
66	59 62 64 65	fsuppco	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((x \circ D))$
67	66	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))$
68	39 58 67	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)\}$
69		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)$
70	31 35 38 68 69	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)$
71		oveq2	$⊢ f = i \to D A f = D A i$
72	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)))$
73		simpr	$⊢ (d = D \land f = i) \to f = i$
74		coeq2	$⊢ d = D \to x \circ d = x \circ D$
75	74	adantr	$⊢ (d = D \land f = i) \to x \circ d = x \circ D$
76	73 75	fveq12d	$⊢ (d = D \land f = i) \to f (x \circ d) = i (x \circ D)$
77	76	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))$
78	77	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))$
79	9	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to D \in P$
80	37	a1i	$⊢ ((φ \land i \in M) \land j \in M) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
81	80	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$
82	72 78 79 28 81	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))$
83	71 82	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))$
84	6 83 28 81	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))$
85		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$
86	84 85	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)$
87		oveq2	$⊢ f = j \to D A f = D A j$
88		simpr	$⊢ (d = D \land f = j) \to f = j$
89	74	adantr	$⊢ (d = D \land f = j) \to x \circ d = x \circ D$
90	88 89	fveq12d	$⊢ (d = D \land f = j) \to f (x \circ d) = j (x \circ D)$
91	90	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))$
92	91	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))$
93	80	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$
94	72 92 79 32 93	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))$
95	87 94	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))$
96	6 95 32 93	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))$
97		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$
98	96 97	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)$
99	86 98	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)$
100	70 99	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)$
101	100	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))$
102	24	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to F : M ⟶ M$
103	102 28	ffvelcdmd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) \in M$
104	7 25 11 27 103	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
105	104	ffnd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
106	102 32	ffvelcdmd	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) \in M$
107	7 25 11 27 106	mplelf	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
108	107	ffnd	$⊢ ((φ \land i \in M) \land j \in M) \to F (j) Fn \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
109	80 105 108	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))$
110	101 109	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)$
111		oveq2	$⊢ f = i +_{W} j \to D A f = D A (i +_{W} j)$
112		simpr	$⊢ (d = D \land f = i +_{W} j) \to f = i +_{W} j$
113	74	adantr	$⊢ (d = D \land f = i +_{W} j) \to x \circ d = x \circ D$
114	112 113	fveq12d	$⊢ (d = D \land f = i +_{W} j) \to f (x \circ d) = (i +_{W} j) (x \circ D)$
115	114	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))$
116	115	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))$
117	15	ad2antrr	$⊢ ((φ \land i \in M) \land j \in M) \to W \in Grp$
118	11 12 117 28 32	grpcld	$⊢ ((φ \land i \in M) \land j \in M) \to i +_{W} j \in M$
119	80	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$
120	72 116 79 118 119	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))$
121	111 120	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))$
122	6 121 118 119	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))$
123		eqid	$⊢ +_{R} = +_{R}$
124	7 11 123 12 28 32	mpladd	$⊢ ((φ \land i \in M) \land j \in M) \to i +_{W} j = i {+_{R}}_{f} j$
125	124	fveq1d	$⊢ ((φ \land i \in M) \land j \in M) \to (i +_{W} j) (x \circ D) = (i {+_{R}}_{f} j) (x \circ D)$
126	125	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))$
127	122 126	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))$
128	7 11 123 12 103 106	mpladd	$⊢ ((φ \land i \in M) \land j \in M) \to F (i) +_{W} F (j) = F (i) {+_{R}}_{f} F (j)$
129	110 127 128	3eqtr4d	$⊢ ((φ \land i \in M) \land j \in M) \to F (i +_{W} j) = F (i) +_{W} F (j)$
130	129	anasss	$⊢ (φ \land (i \in M \land j \in M)) \to F (i +_{W} j) = F (i) +_{W} F (j)$
131		simpr	$⊢ (φ \land f = 0_{W}) \to f = 0_{W}$
132	131	oveq2d	$⊢ (φ \land f = 0_{W}) \to D A f = D A 0_{W}$
133	4	a1i	$⊢ φ \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
134		simplrr	$⊢ ((φ \land (d = D \land f = 0_{W})) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f = 0_{W}$
135		eqid	$⊢ 0_{R} = 0_{R}$
136	8	ringgrpd	$⊢ φ \to R \in Grp$
137	7 27 135 13 5 136	mpl0	$⊢ φ \to 0_{W} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\}$
138	137	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}\}$
139	134 138	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}\}$
140	74	ad2antrl	$⊢ (φ \land (d = D \land f = 0_{W})) \to x \circ d = x \circ D$
141	140	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$
142	139 141	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)$
143	142	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))$
144	55	adantr	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to D : I ⟶ I$
145	50 144	fcod	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \circ D) : I ⟶ ℕ_{0}$
146	44 43 145	elmapdd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in ({ℕ_{0}}^{I})$
147	39 146 66	elrabd	$⊢ (φ \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ D \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
148		fvex	$⊢ 0_{R} \in V$
149	148	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}$
150	147 149	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}$
151	150	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})$
152		fconstmpt	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \times \{0_{R}\} = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 0_{R})$
153	137 152	eqtrdi	$⊢ φ \to 0_{W} = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 0_{R})$
154	151 153	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}$
155	154	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}$
156	143 155	eqtrd	$⊢ (φ \land (d = D \land f = 0_{W})) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = 0_{W}$
157	11 13	grpidcl	$⊢ W \in Grp \to 0_{W} \in M$
158	15 157	syl	$⊢ φ \to 0_{W} \in M$
159	133 156 9 158 158	ovmpod	$⊢ φ \to D A 0_{W} = 0_{W}$
160	159	adantr	$⊢ (φ \land f = 0_{W}) \to D A 0_{W} = 0_{W}$
161	132 160	eqtrd	$⊢ (φ \land f = 0_{W}) \to D A f = 0_{W}$
162	6 161 158 158	fvmptd2	$⊢ φ \to F (0_{W}) = 0_{W}$
163	11 11 12 12 13 13 16 16 24 130 162	ismhmd	$⊢ φ \to F \in (W MndHom W)$

Metamath Proof Explorer

Theorem mplvrpmmhm

Proof