mplvrpmga

Description: The action of permuting variables in a multivariate polynomial is a group action. (Contributed by Thierry Arnoux, 10-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$
Assertion	mplvrpmga	$⊢ φ \to A \in (S GrpAct M)$

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	1	symggrp	$⊢ I \in V \to S \in Grp$
7	5 6	syl	$⊢ φ \to S \in Grp$
8	3	fvexi	$⊢ M \in V$
9	8	a1i	$⊢ φ \to M \in V$
10		fvexd	$⊢ (φ \land c \in (P \times M)) \to {Base}_{R} \in V$
11		ovex	$⊢ {ℕ_{0}}^{I} \in V$
12	11	rabex	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
13	12	a1i	$⊢ (φ \land c \in (P \times M)) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
14		eqid	$⊢ I mPoly R = I mPoly R$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
17	16	psrbasfsupp	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
18		xp2nd	$⊢ c \in (P \times M) \to 2^{nd} (c) \in M$
19	18	ad2antlr	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 2^{nd} (c) \in M$
20	14 15 3 17 19	mplelf	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 2^{nd} (c) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
21	5	ad2antrr	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
22		xp1st	$⊢ c \in (P \times M) \to 1^{st} (c) \in P$
23	22	ad2antlr	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 1^{st} (c) \in P$
24		simpr	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
25	1 2 21 23 24	mplvrpmlem	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ 1^{st} (c) \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
26	20 25	ffvelcdmd	$⊢ ((φ \land c \in (P \times M)) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 2^{nd} (c) (x \circ 1^{st} (c)) \in {Base}_{R}$
27	26	fmpttd	$⊢ (φ \land c \in (P \times M)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
28	10 13 27	elmapdd	$⊢ (φ \land c \in (P \times M)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) \in ({Base}_{R}^{\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}})$
29		eqid	$⊢ I mPwSer R = I mPwSer R$
30		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
31	29 15 17 30 5	psrbas	$⊢ φ \to {Base}_{(I mPwSer R)} = {Base}_{R}^{\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}$
32	31	adantr	$⊢ (φ \land c \in (P \times M)) \to {Base}_{(I mPwSer R)} = {Base}_{R}^{\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}$
33	28 32	eleqtrrd	$⊢ (φ \land c \in (P \times M)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) \in {Base}_{(I mPwSer R)}$
34		coeq1	$⊢ x = y \to x \circ 1^{st} (c) = y \circ 1^{st} (c)$
35	34	fveq2d	$⊢ x = y \to 2^{nd} (c) (x \circ 1^{st} (c)) = 2^{nd} (c) (y \circ 1^{st} (c))$
36	35	cbvmptv	$⊢ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ 1^{st} (c)))$
37		fveq1	$⊢ g = 2^{nd} (c) \to g (y \circ q) = 2^{nd} (c) (y \circ q)$
38	37	mpteq2dv	$⊢ g = 2^{nd} (c) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ q))$
39	38	breq1d	$⊢ g = 2^{nd} (c) \to ({finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \leftrightarrow {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ q))))$
40		coeq2	$⊢ q = 1^{st} (c) \to y \circ q = y \circ 1^{st} (c)$
41	40	fveq2d	$⊢ q = 1^{st} (c) \to 2^{nd} (c) (y \circ q) = 2^{nd} (c) (y \circ 1^{st} (c))$
42	41	mpteq2dv	$⊢ q = 1^{st} (c) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ q)) = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ 1^{st} (c)))$
43	42	breq1d	$⊢ q = 1^{st} (c) \to ({finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ q))) \leftrightarrow {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ 1^{st} (c)))))$
44	4	a1i	$⊢ ((φ \land g \in M) \land q \in P) \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
45		simpr	$⊢ (d = q \land f = g) \to f = g$
46		coeq2	$⊢ d = q \to x \circ d = x \circ q$
47	46	adantr	$⊢ (d = q \land f = g) \to x \circ d = x \circ q$
48	45 47	fveq12d	$⊢ (d = q \land f = g) \to f (x \circ d) = g (x \circ q)$
49	48	mpteq2dv	$⊢ (d = q \land f = g) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q))$
50	49	adantl	$⊢ (((φ \land g \in M) \land q \in P) \land (d = q \land f = g)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q))$
51		simpr	$⊢ ((φ \land g \in M) \land q \in P) \to q \in P$
52		simplr	$⊢ ((φ \land g \in M) \land q \in P) \to g \in M$
53	12	mptex	$⊢ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q)) \in V$
54	53	a1i	$⊢ ((φ \land g \in M) \land q \in P) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q)) \in V$
55	44 50 51 52 54	ovmpod	$⊢ ((φ \land g \in M) \land q \in P) \to q A g = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q))$
56		coeq1	$⊢ x = y \to x \circ q = y \circ q$
57	56	fveq2d	$⊢ x = y \to g (x \circ q) = g (y \circ q)$
58	57	cbvmptv	$⊢ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ q)) = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
59	55 58	eqtrdi	$⊢ ((φ \land g \in M) \land q \in P) \to q A g = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
60	5	ad2antrr	$⊢ ((φ \land g \in M) \land q \in P) \to I \in V$
61		eqid	$⊢ 0_{R} = 0_{R}$
62	1 2 3 4 60 61 52 51	mplvrpmfgalem	$⊢ ((φ \land g \in M) \land q \in P) \to {finSupp}_{0_{R}} ((q A g))$
63	59 62	eqbrtrrd	$⊢ ((φ \land g \in M) \land q \in P) \to {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
64	63	anasss	$⊢ (φ \land (g \in M \land q \in P)) \to {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
65	64	ralrimivva	$⊢ φ \to \forall g \in M \forall q \in P {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
66	65	adantr	$⊢ (φ \land c \in (P \times M)) \to \forall g \in M \forall q \in P {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
67	18	adantl	$⊢ (φ \land c \in (P \times M)) \to 2^{nd} (c) \in M$
68	22	adantl	$⊢ (φ \land c \in (P \times M)) \to 1^{st} (c) \in P$
69	39 43 66 67 68	rspc2dv	$⊢ (φ \land c \in (P \times M)) \to {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (y \circ 1^{st} (c))))$
70	36 69	eqbrtrid	$⊢ (φ \land c \in (P \times M)) \to {finSupp}_{0_{R}} ((x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))))$
71	14 29 30 61 3	mplelbas	$⊢ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) \in M \leftrightarrow ((x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) \in {Base}_{(I mPwSer R)} \land {finSupp}_{0_{R}} ((x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c)))))$
72	33 70 71	sylanbrc	$⊢ (φ \land c \in (P \times M)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) \in M$
73		vex	$⊢ d \in V$
74		vex	$⊢ f \in V$
75	73 74	op2ndd	$⊢ c = ⟨d, f⟩ \to 2^{nd} (c) = f$
76	73 74	op1std	$⊢ c = ⟨d, f⟩ \to 1^{st} (c) = d$
77	76	coeq2d	$⊢ c = ⟨d, f⟩ \to x \circ 1^{st} (c) = x \circ d$
78	75 77	fveq12d	$⊢ c = ⟨d, f⟩ \to 2^{nd} (c) (x \circ 1^{st} (c)) = f (x \circ d)$
79	78	mpteq2dv	$⊢ c = ⟨d, f⟩ \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d))$
80	79	mpompt	$⊢ (c \in (P \times M) ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c)))) = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
81	4 80	eqtr4i	$⊢ A = (c \in (P \times M) ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ 2^{nd} (c) (x \circ 1^{st} (c))))$
82	72 81	fmptd	$⊢ φ \to A : P \times M ⟶ M$
83	1	symgid	$⊢ I \in V \to {I ↾}_{I} = 0_{S}$
84	5 83	syl	$⊢ φ \to {I ↾}_{I} = 0_{S}$
85	84	adantr	$⊢ (φ \land g \in M) \to {I ↾}_{I} = 0_{S}$
86	85	oveq1d	$⊢ (φ \land g \in M) \to ({I ↾}_{I}) A g = 0_{S} A g$
87	4	a1i	$⊢ (φ \land g \in M) \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
88		ssrab2	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
89	88	a1i	$⊢ (φ \land g \in M) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
90	89	sselda	$⊢ ((φ \land g \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in ({ℕ_{0}}^{I})$
91	90	elmaprd	$⊢ ((φ \land g \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
92		fcoi1	$⊢ x : I ⟶ ℕ_{0} \to x \circ ({I ↾}_{I}) = x$
93	91 92	syl	$⊢ ((φ \land g \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ ({I ↾}_{I}) = x$
94	93	fveq2d	$⊢ ((φ \land g \in M) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g (x \circ ({I ↾}_{I})) = g (x)$
95	94	mpteq2dva	$⊢ (φ \land g \in M) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ ({I ↾}_{I}))) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x))$
96	95	adantr	$⊢ ((φ \land g \in M) \land (d = {I ↾}_{I} \land f = g)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ ({I ↾}_{I}))) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x))$
97		simpr	$⊢ (d = {I ↾}_{I} \land f = g) \to f = g$
98		coeq2	$⊢ d = {I ↾}_{I} \to x \circ d = x \circ ({I ↾}_{I})$
99	98	adantr	$⊢ (d = {I ↾}_{I} \land f = g) \to x \circ d = x \circ ({I ↾}_{I})$
100	97 99	fveq12d	$⊢ (d = {I ↾}_{I} \land f = g) \to f (x \circ d) = g (x \circ ({I ↾}_{I}))$
101	100	mpteq2dv	$⊢ (d = {I ↾}_{I} \land f = g) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ ({I ↾}_{I})))$
102	101	adantl	$⊢ ((φ \land g \in M) \land (d = {I ↾}_{I} \land f = g)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ ({I ↾}_{I})))$
103	14 29 30 61 3	mplelbas	$⊢ g \in M \leftrightarrow (g \in {Base}_{(I mPwSer R)} \land {finSupp}_{0_{R}} (g))$
104	103	simplbi	$⊢ g \in M \to g \in {Base}_{(I mPwSer R)}$
105	29 15 17 30 104	psrelbas	$⊢ g \in M \to g : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
106	105	ad3antlr	$⊢ (((φ \land g \in M) \land d = {I ↾}_{I}) \land f = g) \to g : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
107	106	feqmptd	$⊢ (((φ \land g \in M) \land d = {I ↾}_{I}) \land f = g) \to g = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x))$
108	107	anasss	$⊢ ((φ \land g \in M) \land (d = {I ↾}_{I} \land f = g)) \to g = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x))$
109	96 102 108	3eqtr4d	$⊢ ((φ \land g \in M) \land (d = {I ↾}_{I} \land f = g)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = g$
110		eqid	$⊢ 0_{S} = 0_{S}$
111	2 110	grpidcl	$⊢ S \in Grp \to 0_{S} \in P$
112	5 6 111	3syl	$⊢ φ \to 0_{S} \in P$
113	84 112	eqeltrd	$⊢ φ \to {I ↾}_{I} \in P$
114	113	adantr	$⊢ (φ \land g \in M) \to {I ↾}_{I} \in P$
115		simpr	$⊢ (φ \land g \in M) \to g \in M$
116	87 109 114 115 115	ovmpod	$⊢ (φ \land g \in M) \to ({I ↾}_{I}) A g = g$
117	86 116	eqtr3d	$⊢ (φ \land g \in M) \to 0_{S} A g = g$
118		eqid	$⊢ +_{S} = +_{S}$
119	1 2 118	symgov	$⊢ (p \in P \land q \in P) \to p +_{S} q = p \circ q$
120	119	adantll	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p +_{S} q = p \circ q$
121	120	oveq1d	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (p +_{S} q) A g = (p \circ q) A g$
122		coass	$⊢ (x \circ p) \circ q = x \circ (p \circ q)$
123	122	a1i	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \circ p) \circ q = x \circ (p \circ q)$
124	123	fveq2d	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g ((x \circ p) \circ q) = g (x \circ (p \circ q))$
125	124	mpteq2dva	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ (p \circ q)))$
126	59	adantlr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to q A g = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
127	126	oveq2d	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p A (q A g) = p A (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
128	4	a1i	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to A = (d \in P, f \in M ⟼ (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)))$
129		simpllr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to d = p$
130	129	coeq2d	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ d = x \circ p$
131	130	fveq2d	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f (x \circ d) = f (x \circ p)$
132		simplr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
133		simpr	$⊢ (((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land y = x \circ p) \to y = x \circ p$
134	133	coeq1d	$⊢ (((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land y = x \circ p) \to y \circ q = (x \circ p) \circ q$
135	134	fveq2d	$⊢ (((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \land y = x \circ p) \to g (y \circ q) = g ((x \circ p) \circ q)$
136		breq1	$⊢ h = x \circ p \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((x \circ p)))$
137		nn0ex	$⊢ ℕ_{0} \in V$
138	137	a1i	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
139	5	ad3antrrr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to I \in V$
140	139	ad3antrrr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
141	88	a1i	$⊢ (((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
142	141	sselda	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in ({ℕ_{0}}^{I})$
143	142	elmaprd	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x : I ⟶ ℕ_{0}$
144	1 2	symgbasf	$⊢ p \in P \to p : I ⟶ I$
145	144	ad5antlr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to p : I ⟶ I$
146	143 145	fcod	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (x \circ p) : I ⟶ ℕ_{0}$
147	138 140 146	elmapdd	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ p \in ({ℕ_{0}}^{I})$
148		breq1	$⊢ h = x \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (x))$
149	148	elrab	$⊢ x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \leftrightarrow (x \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (x))$
150	149	simprbi	$⊢ x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \to {finSupp}_{0} (x)$
151	150	adantl	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (x)$
152	1 2	symgbasf1o	$⊢ p \in P \to p : I \underset{1-1 onto}{⟶} I$
153		f1of1	$⊢ p : I \underset{1-1 onto}{⟶} I \to p : I \underset{1-1}{⟶} I$
154	152 153	syl	$⊢ p \in P \to p : I \underset{1-1}{⟶} I$
155	154	ad5antlr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to p : I \underset{1-1}{⟶} I$
156		0nn0	$⊢ 0 \in ℕ_{0}$
157	156	a1i	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
158		simpr	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
159	151 155 157 158	fsuppco	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((x \circ p))$
160	136 147 159	elrabd	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to x \circ p \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
161		fvexd	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g ((x \circ p) \circ q) \in V$
162		nfv	$⊢ Ⅎ y ((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p)$
163		nfmpt1	$⊢ \underline{Ⅎ} y (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
164	163	nfeq2	$⊢ Ⅎ y f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))$
165	162 164	nfan	$⊢ Ⅎ y (((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
166		nfv	$⊢ Ⅎ y x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
167	165 166	nfan	$⊢ Ⅎ y ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\})$
168		nfcv	$⊢ \underline{Ⅎ} y (x \circ p)$
169		nfcv	$⊢ \underline{Ⅎ} y g ((x \circ p) \circ q)$
170	132 135 160 161 167 168 169	fvmptdf	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f (x \circ p) = g ((x \circ p) \circ q)$
171	131 170	eqtrd	$⊢ ((((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \land x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to f (x \circ d) = g ((x \circ p) \circ q)$
172	171	mpteq2dva	$⊢ (((((φ \land g \in M) \land p \in P) \land q \in P) \land d = p) \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q))$
173	172	anasss	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land (d = p \land f = (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q))$
174		simplr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p \in P$
175		fvexd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to {Base}_{R} \in V$
176	12	a1i	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \in V$
177	115	ad3antrrr	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g \in M$
178	14 15 3 17 177	mplelf	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
179		breq1	$⊢ h = y \circ q \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} ((y \circ q)))$
180	137	a1i	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to ℕ_{0} \in V$
181	139	adantr	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to I \in V$
182	88	a1i	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \subseteq {ℕ_{0}}^{I}$
183	182	sselda	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to y \in ({ℕ_{0}}^{I})$
184	183	elmaprd	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to y : I ⟶ ℕ_{0}$
185	1 2	symgbasf	$⊢ q \in P \to q : I ⟶ I$
186	185	ad2antlr	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to q : I ⟶ I$
187	184 186	fcod	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to (y \circ q) : I ⟶ ℕ_{0}$
188	180 181 187	elmapdd	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to y \circ q \in ({ℕ_{0}}^{I})$
189		breq1	$⊢ h = y \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (y))$
190	189	elrab	$⊢ y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \leftrightarrow (y \in ({ℕ_{0}}^{I}) \land {finSupp}_{0} (y))$
191	190	simprbi	$⊢ y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} \to {finSupp}_{0} (y)$
192	191	adantl	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} (y)$
193	1 2	symgbasf1o	$⊢ q \in P \to q : I \underset{1-1 onto}{⟶} I$
194	193	ad2antlr	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to q : I \underset{1-1 onto}{⟶} I$
195		f1of1	$⊢ q : I \underset{1-1 onto}{⟶} I \to q : I \underset{1-1}{⟶} I$
196	194 195	syl	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to q : I \underset{1-1}{⟶} I$
197	156	a1i	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to 0 \in ℕ_{0}$
198		simpr	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
199	192 196 197 198	fsuppco	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to {finSupp}_{0} ((y \circ q))$
200	179 188 199	elrabd	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to y \circ q \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
201	178 200	ffvelcdmd	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}) \to g (y \circ q) \in {Base}_{R}$
202	201	fmpttd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) : \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟶ {Base}_{R}$
203	175 176 202	elmapdd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) \in ({Base}_{R}^{\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}})$
204	31	ad3antrrr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to {Base}_{(I mPwSer R)} = {Base}_{R}^{\{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}}$
205	203 204	eleqtrrd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) \in {Base}_{(I mPwSer R)}$
206	63	adantlr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)))$
207	14 29 30 61 3	mplelbas	$⊢ (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) \in M \leftrightarrow ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) \in {Base}_{(I mPwSer R)} \land {finSupp}_{0_{R}} ((y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q))))$
208	205 206 207	sylanbrc	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) \in M$
209	176	mptexd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q)) \in V$
210	128 173 174 208 209	ovmpod	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p A (y \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (y \circ q)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q))$
211	127 210	eqtrd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p A (q A g) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g ((x \circ p) \circ q))$
212		simpr	$⊢ (d = p \circ q \land f = g) \to f = g$
213		coeq2	$⊢ d = p \circ q \to x \circ d = x \circ (p \circ q)$
214	213	adantr	$⊢ (d = p \circ q \land f = g) \to x \circ d = x \circ (p \circ q)$
215	212 214	fveq12d	$⊢ (d = p \circ q \land f = g) \to f (x \circ d) = g (x \circ (p \circ q))$
216	215	mpteq2dv	$⊢ (d = p \circ q \land f = g) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ (p \circ q)))$
217	216	adantl	$⊢ ((((φ \land g \in M) \land p \in P) \land q \in P) \land (d = p \circ q \land f = g)) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ f (x \circ d)) = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ (p \circ q)))$
218	139 6	syl	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to S \in Grp$
219		simpr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to q \in P$
220	2 118 218 174 219	grpcld	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p +_{S} q \in P$
221	120 220	eqeltrrd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to p \circ q \in P$
222		simpllr	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to g \in M$
223	176	mptexd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ (p \circ q))) \in V$
224	128 217 221 222 223	ovmpod	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (p \circ q) A g = (x \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} ⟼ g (x \circ (p \circ q)))$
225	125 211 224	3eqtr4rd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (p \circ q) A g = p A (q A g)$
226	121 225	eqtrd	$⊢ (((φ \land g \in M) \land p \in P) \land q \in P) \to (p +_{S} q) A g = p A (q A g)$
227	226	anasss	$⊢ ((φ \land g \in M) \land (p \in P \land q \in P)) \to (p +_{S} q) A g = p A (q A g)$
228	227	ralrimivva	$⊢ (φ \land g \in M) \to \forall p \in P \forall q \in P (p +_{S} q) A g = p A (q A g)$
229	117 228	jca	$⊢ (φ \land g \in M) \to (0_{S} A g = g \land \forall p \in P \forall q \in P (p +_{S} q) A g = p A (q A g))$
230	229	ralrimiva	$⊢ φ \to \forall g \in M (0_{S} A g = g \land \forall p \in P \forall q \in P (p +_{S} q) A g = p A (q A g))$
231	2 118 110	isga	$⊢ A \in (S GrpAct M) \leftrightarrow ((S \in Grp \land M \in V) \land (A : P \times M ⟶ M \land \forall g \in M (0_{S} A g = g \land \forall p \in P \forall q \in P (p +_{S} q) A g = p A (q A g))))$
232	7 9 82 230 231	syl22anbrc	$⊢ φ \to A \in (S GrpAct M)$

Metamath Proof Explorer

Theorem mplvrpmga

Proof