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

Metamath Proof Explorer

Theorem mplvrpmga

Proof