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

Metamath Proof Explorer

Theorem mplvrpmmhm

Proof