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	⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
	mplvrpmga.2	⊢ 𝑃 = ( Base ‘ 𝑆 )
	mplvrpmga.3	⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
	mplvrpmga.4	⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
	mplvrpmga.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
Assertion	mplvrpmga	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		mplvrpmga.1	⊢ 𝑆 = ( SymGrp ‘ 𝐼 )
2		mplvrpmga.2	⊢ 𝑃 = ( Base ‘ 𝑆 )
3		mplvrpmga.3	⊢ 𝑀 = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
4		mplvrpmga.4	⊢ 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
5		mplvrpmga.5	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6	1	symggrp	⊢ ( 𝐼 ∈ 𝑉 → 𝑆 ∈ Grp )
7	5 6	syl	⊢ ( 𝜑 → 𝑆 ∈ Grp )
8	3	fvexi	⊢ 𝑀 ∈ V
9	8	a1i	⊢ ( 𝜑 → 𝑀 ∈ V )
10		fvexd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( Base ‘ 𝑅 ) ∈ V )
11		ovex	⊢ ( ℕ₀ ↑_m 𝐼 ) ∈ V
12	11	rabex	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
14		eqid	⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16		eqid	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
17	16	psrbasfsupp	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
18		xp2nd	⊢ ( 𝑐 ∈ ( 𝑃 × 𝑀 ) → ( 2^nd ‘ 𝑐 ) ∈ 𝑀 )
19	18	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 2^nd ‘ 𝑐 ) ∈ 𝑀 )
20	14 15 3 17 19	mplelf	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 2^nd ‘ 𝑐 ) : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
21		breq1	⊢ ( ℎ = ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) → ( ℎ finSupp 0 ↔ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) finSupp 0 ) )
22		nn0ex	⊢ ℕ₀ ∈ V
23	22	a1i	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ₀ ∈ V )
24	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
25		ssrab2	⊢ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 )
26	25	a1i	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 ) )
27	26	sselda	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ ( ℕ₀ ↑_m 𝐼 ) )
28	24 23 27	elmaprd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ₀ )
29		xp1st	⊢ ( 𝑐 ∈ ( 𝑃 × 𝑀 ) → ( 1^st ‘ 𝑐 ) ∈ 𝑃 )
30	29	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 1^st ‘ 𝑐 ) ∈ 𝑃 )
31	1 2	symgbasf	⊢ ( ( 1^st ‘ 𝑐 ) ∈ 𝑃 → ( 1^st ‘ 𝑐 ) : 𝐼 ⟶ 𝐼 )
32	30 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 1^st ‘ 𝑐 ) : 𝐼 ⟶ 𝐼 )
33	28 32	fcod	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) : 𝐼 ⟶ ℕ₀ )
34	23 24 33	elmapdd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ∈ ( ℕ₀ ↑_m 𝐼 ) )
35		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
36		breq1	⊢ ( ℎ = 𝑥 → ( ℎ finSupp 0 ↔ 𝑥 finSupp 0 ) )
37	36	elrab	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↔ ( 𝑥 ∈ ( ℕ₀ ↑_m 𝐼 ) ∧ 𝑥 finSupp 0 ) )
38	35 37	sylib	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∈ ( ℕ₀ ↑_m 𝐼 ) ∧ 𝑥 finSupp 0 ) )
39	38	simprd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 finSupp 0 )
40	1 2	symgbasf1o	⊢ ( ( 1^st ‘ 𝑐 ) ∈ 𝑃 → ( 1^st ‘ 𝑐 ) : 𝐼 –1-1-onto→ 𝐼 )
41		f1of1	⊢ ( ( 1^st ‘ 𝑐 ) : 𝐼 –1-1-onto→ 𝐼 → ( 1^st ‘ 𝑐 ) : 𝐼 –1-1→ 𝐼 )
42	30 40 41	3syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 1^st ‘ 𝑐 ) : 𝐼 –1-1→ 𝐼 )
43		0nn0	⊢ 0 ∈ ℕ₀
44	43	a1i	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ₀ )
45	39 42 44 35	fsuppco	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) finSupp 0 )
46	21 34 45	elrabd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
47	20 46	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ∈ ( Base ‘ 𝑅 ) )
48	47	fmpttd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
49	10 13 48	elmapdd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑_m { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) )
50		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
51		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
52	50 15 17 51 5	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑_m { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑_m { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) )
54	49 53	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
55		coeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) = ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) )
56	55	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) )
57	56	cbvmptv	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) )
58		fveq1	⊢ ( 𝑔 = ( 2^nd ‘ 𝑐 ) → ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) )
59	58	mpteq2dv	⊢ ( 𝑔 = ( 2^nd ‘ 𝑐 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) ) )
60	59	breq1d	⊢ ( 𝑔 = ( 2^nd ‘ 𝑐 ) → ( ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) ↔ ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) ) )
61		coeq2	⊢ ( 𝑞 = ( 1^st ‘ 𝑐 ) → ( 𝑦 ∘ 𝑞 ) = ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) )
62	61	fveq2d	⊢ ( 𝑞 = ( 1^st ‘ 𝑐 ) → ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) )
63	62	mpteq2dv	⊢ ( 𝑞 = ( 1^st ‘ 𝑐 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) ) )
64	63	breq1d	⊢ ( 𝑞 = ( 1^st ‘ 𝑐 ) → ( ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) ↔ ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) ) )
65	4	a1i	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
66		simpr	⊢ ( ( 𝑑 = 𝑞 ∧ 𝑓 = 𝑔 ) → 𝑓 = 𝑔 )
67		coeq2	⊢ ( 𝑑 = 𝑞 → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑞 ) )
68	67	adantr	⊢ ( ( 𝑑 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑞 ) )
69	66 68	fveq12d	⊢ ( ( 𝑑 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) )
70	69	mpteq2dv	⊢ ( ( 𝑑 = 𝑞 ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) )
71	70	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑑 = 𝑞 ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) )
72		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑞 ∈ 𝑃 )
73		simplr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑔 ∈ 𝑀 )
74	12	mptex	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) ∈ V
75	74	a1i	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) ∈ V )
76	65 71 72 73 75	ovmpod	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑞 𝐴 𝑔 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) )
77		coeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∘ 𝑞 ) = ( 𝑦 ∘ 𝑞 ) )
78	77	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) = ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) )
79	78	cbvmptv	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ 𝑞 ) ) ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) )
80	76 79	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑞 𝐴 𝑔 ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) )
81	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → 𝐼 ∈ 𝑉 )
82		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
83	1 2 3 4 81 82 73 72	mplvrpmfgalem	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑞 𝐴 𝑔 ) finSupp ( 0_g ‘ 𝑅 ) )
84	80 83	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
85	84	anasss	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝑀 ∧ 𝑞 ∈ 𝑃 ) ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
86	85	ralrimivva	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝑀 ∀ 𝑞 ∈ 𝑃 ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
87	86	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ∀ 𝑔 ∈ 𝑀 ∀ 𝑞 ∈ 𝑃 ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
88	18	adantl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 2^nd ‘ 𝑐 ) ∈ 𝑀 )
89	29	adantl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 1^st ‘ 𝑐 ) ∈ 𝑃 )
90	60 64 87 88 89	rspc2dv	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑦 ∘ ( 1^st ‘ 𝑐 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
91	57 90	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
92	14 50 51 82 3	mplelbas	⊢ ( ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ∈ 𝑀 ↔ ( ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) finSupp ( 0_g ‘ 𝑅 ) ) )
93	54 91 92	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝑃 × 𝑀 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ∈ 𝑀 )
94		vex	⊢ 𝑑 ∈ V
95		vex	⊢ 𝑓 ∈ V
96	94 95	op2ndd	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑓 ⟩ → ( 2^nd ‘ 𝑐 ) = 𝑓 )
97	94 95	op1std	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑓 ⟩ → ( 1^st ‘ 𝑐 ) = 𝑑 )
98	97	coeq2d	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑓 ⟩ → ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) = ( 𝑥 ∘ 𝑑 ) )
99	96 98	fveq12d	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑓 ⟩ → ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) = ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) )
100	99	mpteq2dv	⊢ ( 𝑐 = ⟨ 𝑑 , 𝑓 ⟩ → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
101	100	mpompt	⊢ ( 𝑐 ∈ ( 𝑃 × 𝑀 ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) ) = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) )
102	4 101	eqtr4i	⊢ 𝐴 = ( 𝑐 ∈ ( 𝑃 × 𝑀 ) ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑥 ∘ ( 1^st ‘ 𝑐 ) ) ) ) )
103	93 102	fmptd	⊢ ( 𝜑 → 𝐴 : ( 𝑃 × 𝑀 ) ⟶ 𝑀 )
104	1	symgid	⊢ ( 𝐼 ∈ 𝑉 → ( I ↾ 𝐼 ) = ( 0_g ‘ 𝑆 ) )
105	5 104	syl	⊢ ( 𝜑 → ( I ↾ 𝐼 ) = ( 0_g ‘ 𝑆 ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( I ↾ 𝐼 ) = ( 0_g ‘ 𝑆 ) )
107	106	oveq1d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( ( I ↾ 𝐼 ) 𝐴 𝑔 ) = ( ( 0_g ‘ 𝑆 ) 𝐴 𝑔 ) )
108	4	a1i	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
109	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
110	22	a1i	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ₀ ∈ V )
111	25	a1i	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 ) )
112	111	sselda	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ ( ℕ₀ ↑_m 𝐼 ) )
113	109 110 112	elmaprd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ₀ )
114		fcoi1	⊢ ( 𝑥 : 𝐼 ⟶ ℕ₀ → ( 𝑥 ∘ ( I ↾ 𝐼 ) ) = 𝑥 )
115	113 114	syl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ ( I ↾ 𝐼 ) ) = 𝑥 )
116	115	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) = ( 𝑔 ‘ 𝑥 ) )
117	116	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ 𝑥 ) ) )
118	117	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ 𝑥 ) ) )
119		simpr	⊢ ( ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) → 𝑓 = 𝑔 )
120		coeq2	⊢ ( 𝑑 = ( I ↾ 𝐼 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ ( I ↾ 𝐼 ) ) )
121	120	adantr	⊢ ( ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ ( I ↾ 𝐼 ) ) )
122	119 121	fveq12d	⊢ ( ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) )
123	122	mpteq2dv	⊢ ( ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) ) )
124	123	adantl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( I ↾ 𝐼 ) ) ) ) )
125	14 50 51 82 3	mplelbas	⊢ ( 𝑔 ∈ 𝑀 ↔ ( 𝑔 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑔 finSupp ( 0_g ‘ 𝑅 ) ) )
126	125	simplbi	⊢ ( 𝑔 ∈ 𝑀 → 𝑔 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
127	50 15 17 51 126	psrelbas	⊢ ( 𝑔 ∈ 𝑀 → 𝑔 : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
128	127	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑑 = ( I ↾ 𝐼 ) ) ∧ 𝑓 = 𝑔 ) → 𝑔 : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
129	128	feqmptd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑑 = ( I ↾ 𝐼 ) ) ∧ 𝑓 = 𝑔 ) → 𝑔 = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ 𝑥 ) ) )
130	129	anasss	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) ) → 𝑔 = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ 𝑥 ) ) )
131	118 124 130	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ ( 𝑑 = ( I ↾ 𝐼 ) ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = 𝑔 )
132		eqid	⊢ ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑆 )
133	2 132	grpidcl	⊢ ( 𝑆 ∈ Grp → ( 0_g ‘ 𝑆 ) ∈ 𝑃 )
134	5 6 133	3syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑆 ) ∈ 𝑃 )
135	105 134	eqeltrd	⊢ ( 𝜑 → ( I ↾ 𝐼 ) ∈ 𝑃 )
136	135	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( I ↾ 𝐼 ) ∈ 𝑃 )
137		simpr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → 𝑔 ∈ 𝑀 )
138	108 131 136 137 137	ovmpod	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( ( I ↾ 𝐼 ) 𝐴 𝑔 ) = 𝑔 )
139	107 138	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( ( 0_g ‘ 𝑆 ) 𝐴 𝑔 ) = 𝑔 )
140		eqid	⊢ ( +_g ‘ 𝑆 ) = ( +_g ‘ 𝑆 )
141	1 2 140	symgov	⊢ ( ( 𝑝 ∈ 𝑃 ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) = ( 𝑝 ∘ 𝑞 ) )
142	141	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) = ( 𝑝 ∘ 𝑞 ) )
143	142	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( ( 𝑝 ∘ 𝑞 ) 𝐴 𝑔 ) )
144		coass	⊢ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) = ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) )
145	144	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) = ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) )
146	145	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) = ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) )
147	146	mpteq2dva	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) ) )
148	80	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑞 𝐴 𝑔 ) = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) )
149	148	oveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) = ( 𝑝 𝐴 ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) )
150	4	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝐴 = ( 𝑑 ∈ 𝑃 , 𝑓 ∈ 𝑀 ↦ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) ) )
151		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑑 = 𝑝 )
152	151	coeq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ 𝑝 ) )
153	152	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑓 ‘ ( 𝑥 ∘ 𝑝 ) ) )
154		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) )
155		simpr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑦 = ( 𝑥 ∘ 𝑝 ) ) → 𝑦 = ( 𝑥 ∘ 𝑝 ) )
156	155	coeq1d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑦 = ( 𝑥 ∘ 𝑝 ) ) → ( 𝑦 ∘ 𝑞 ) = ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) )
157	156	fveq2d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) ∧ 𝑦 = ( 𝑥 ∘ 𝑝 ) ) → ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) = ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) )
158		breq1	⊢ ( ℎ = ( 𝑥 ∘ 𝑝 ) → ( ℎ finSupp 0 ↔ ( 𝑥 ∘ 𝑝 ) finSupp 0 ) )
159	22	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ₀ ∈ V )
160	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝐼 ∈ 𝑉 )
161	160	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
162	25	a1i	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 ) )
163	162	sselda	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ ( ℕ₀ ↑_m 𝐼 ) )
164	161 159 163	elmaprd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 : 𝐼 ⟶ ℕ₀ )
165	1 2	symgbasf	⊢ ( 𝑝 ∈ 𝑃 → 𝑝 : 𝐼 ⟶ 𝐼 )
166	165	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 : 𝐼 ⟶ 𝐼 )
167	164 166	fcod	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑝 ) : 𝐼 ⟶ ℕ₀ )
168	159 161 167	elmapdd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑝 ) ∈ ( ℕ₀ ↑_m 𝐼 ) )
169	37	simprbi	⊢ ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } → 𝑥 finSupp 0 )
170	169	adantl	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 finSupp 0 )
171	1 2	symgbasf1o	⊢ ( 𝑝 ∈ 𝑃 → 𝑝 : 𝐼 –1-1-onto→ 𝐼 )
172		f1of1	⊢ ( 𝑝 : 𝐼 –1-1-onto→ 𝐼 → 𝑝 : 𝐼 –1-1→ 𝐼 )
173	171 172	syl	⊢ ( 𝑝 ∈ 𝑃 → 𝑝 : 𝐼 –1-1→ 𝐼 )
174	173	ad5antlr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑝 : 𝐼 –1-1→ 𝐼 )
175	43	a1i	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ₀ )
176		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
177	170 174 175 176	fsuppco	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑝 ) finSupp 0 )
178	158 168 177	elrabd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑥 ∘ 𝑝 ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
179		fvexd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ∈ V )
180		nfv	⊢ Ⅎ 𝑦 ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 )
181		nfmpt1	⊢ Ⅎ 𝑦 ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) )
182	181	nfeq2	⊢ Ⅎ 𝑦 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) )
183	180 182	nfan	⊢ Ⅎ 𝑦 ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) )
184		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 }
185	183 184	nfan	⊢ Ⅎ 𝑦 ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
186		nfcv	⊢ Ⅎ 𝑦 ( 𝑥 ∘ 𝑝 )
187		nfcv	⊢ Ⅎ 𝑦 ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) )
188	154 157 178 179 185 186 187	fvmptdf	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑝 ) ) = ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) )
189	153 188	eqtrd	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ∧ 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) )
190	189	mpteq2dva	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑑 = 𝑝 ) ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) )
191	190	anasss	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑑 = 𝑝 ∧ 𝑓 = ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) )
192		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑝 ∈ 𝑃 )
193		fvexd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( Base ‘ 𝑅 ) ∈ V )
194	12	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ∈ V )
195	137	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑔 ∈ 𝑀 )
196	14 15 3 17 195	mplelf	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑔 : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
197		breq1	⊢ ( ℎ = ( 𝑦 ∘ 𝑞 ) → ( ℎ finSupp 0 ↔ ( 𝑦 ∘ 𝑞 ) finSupp 0 ) )
198	22	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ℕ₀ ∈ V )
199	160	adantr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝐼 ∈ 𝑉 )
200	25	a1i	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⊆ ( ℕ₀ ↑_m 𝐼 ) )
201	200	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑦 ∈ ( ℕ₀ ↑_m 𝐼 ) )
202	199 198 201	elmaprd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑦 : 𝐼 ⟶ ℕ₀ )
203	1 2	symgbasf	⊢ ( 𝑞 ∈ 𝑃 → 𝑞 : 𝐼 ⟶ 𝐼 )
204	203	ad2antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑞 : 𝐼 ⟶ 𝐼 )
205	202 204	fcod	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑦 ∘ 𝑞 ) : 𝐼 ⟶ ℕ₀ )
206	198 199 205	elmapdd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑦 ∘ 𝑞 ) ∈ ( ℕ₀ ↑_m 𝐼 ) )
207		breq1	⊢ ( ℎ = 𝑦 → ( ℎ finSupp 0 ↔ 𝑦 finSupp 0 ) )
208	207	elrab	⊢ ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↔ ( 𝑦 ∈ ( ℕ₀ ↑_m 𝐼 ) ∧ 𝑦 finSupp 0 ) )
209	208	simprbi	⊢ ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } → 𝑦 finSupp 0 )
210	209	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑦 finSupp 0 )
211	1 2	symgbasf1o	⊢ ( 𝑞 ∈ 𝑃 → 𝑞 : 𝐼 –1-1-onto→ 𝐼 )
212	211	ad2antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑞 : 𝐼 –1-1-onto→ 𝐼 )
213		f1of1	⊢ ( 𝑞 : 𝐼 –1-1-onto→ 𝐼 → 𝑞 : 𝐼 –1-1→ 𝐼 )
214	212 213	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑞 : 𝐼 –1-1→ 𝐼 )
215	43	a1i	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 0 ∈ ℕ₀ )
216		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
217	210 214 215 216	fsuppco	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑦 ∘ 𝑞 ) finSupp 0 )
218	197 206 217	elrabd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑦 ∘ 𝑞 ) ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } )
219	196 218	ffvelcdmd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) → ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ∈ ( Base ‘ 𝑅 ) )
220	219	fmpttd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) : { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ⟶ ( Base ‘ 𝑅 ) )
221	193 194 220	elmapdd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ∈ ( ( Base ‘ 𝑅 ) ↑_m { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) )
222	52	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑_m { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ) )
223	221 222	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
224	84	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) )
225	14 50 51 82 3	mplelbas	⊢ ( ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ∈ 𝑀 ↔ ( ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) finSupp ( 0_g ‘ 𝑅 ) ) )
226	223 224 225	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ∈ 𝑀 )
227	194	mptexd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) ∈ V )
228	150 191 192 226 227	ovmpod	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 𝐴 ( 𝑦 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑦 ∘ 𝑞 ) ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) )
229	149 228	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( ( 𝑥 ∘ 𝑝 ) ∘ 𝑞 ) ) ) )
230		simpr	⊢ ( ( 𝑑 = ( 𝑝 ∘ 𝑞 ) ∧ 𝑓 = 𝑔 ) → 𝑓 = 𝑔 )
231		coeq2	⊢ ( 𝑑 = ( 𝑝 ∘ 𝑞 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) )
232	231	adantr	⊢ ( ( 𝑑 = ( 𝑝 ∘ 𝑞 ) ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∘ 𝑑 ) = ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) )
233	230 232	fveq12d	⊢ ( ( 𝑑 = ( 𝑝 ∘ 𝑞 ) ∧ 𝑓 = 𝑔 ) → ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) = ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) )
234	233	mpteq2dv	⊢ ( ( 𝑑 = ( 𝑝 ∘ 𝑞 ) ∧ 𝑓 = 𝑔 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) ) )
235	234	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑑 = ( 𝑝 ∘ 𝑞 ) ∧ 𝑓 = 𝑔 ) ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑓 ‘ ( 𝑥 ∘ 𝑑 ) ) ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) ) )
236	160 6	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑆 ∈ Grp )
237		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑞 ∈ 𝑃 )
238	2 140 236 192 237	grpcld	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) ∈ 𝑃 )
239	142 238	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑝 ∘ 𝑞 ) ∈ 𝑃 )
240		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → 𝑔 ∈ 𝑀 )
241	194	mptexd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) ) ∈ V )
242	150 235 239 240 241	ovmpod	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( 𝑝 ∘ 𝑞 ) 𝐴 𝑔 ) = ( 𝑥 ∈ { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ℎ finSupp 0 } ↦ ( 𝑔 ‘ ( 𝑥 ∘ ( 𝑝 ∘ 𝑞 ) ) ) ) )
243	147 229 242	3eqtr4rd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( 𝑝 ∘ 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) )
244	143 243	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑞 ∈ 𝑃 ) → ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) )
245	244	anasss	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) ∧ ( 𝑝 ∈ 𝑃 ∧ 𝑞 ∈ 𝑃 ) ) → ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) )
246	245	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ∀ 𝑝 ∈ 𝑃 ∀ 𝑞 ∈ 𝑃 ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) )
247	139 246	jca	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑀 ) → ( ( ( 0_g ‘ 𝑆 ) 𝐴 𝑔 ) = 𝑔 ∧ ∀ 𝑝 ∈ 𝑃 ∀ 𝑞 ∈ 𝑃 ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) ) )
248	247	ralrimiva	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝑀 ( ( ( 0_g ‘ 𝑆 ) 𝐴 𝑔 ) = 𝑔 ∧ ∀ 𝑝 ∈ 𝑃 ∀ 𝑞 ∈ 𝑃 ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) ) )
249	2 140 132	isga	⊢ ( 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) ↔ ( ( 𝑆 ∈ Grp ∧ 𝑀 ∈ V ) ∧ ( 𝐴 : ( 𝑃 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑔 ∈ 𝑀 ( ( ( 0_g ‘ 𝑆 ) 𝐴 𝑔 ) = 𝑔 ∧ ∀ 𝑝 ∈ 𝑃 ∀ 𝑞 ∈ 𝑃 ( ( 𝑝 ( +_g ‘ 𝑆 ) 𝑞 ) 𝐴 𝑔 ) = ( 𝑝 𝐴 ( 𝑞 𝐴 𝑔 ) ) ) ) ) )
250	7 9 103 248 249	syl22anbrc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑆 GrpAct 𝑀 ) )

Metamath Proof Explorer

Theorem mplvrpmga

Proof