Theorem mplvrpmga 34170

Description: The action of permuting variables in a multivariate polynomial is a group action. (Contributed by Thierry Arnoux, 10-Jan-2026.)

Hypotheses

Ref	Expression
mplvrpmga.1	⊢ 𝑆 = (SymGrp‘𝐼)
mplvrpmga.2	⊢ 𝑃 = (Base‘𝑆)
mplvrpmga.3	⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))
mplvrpmga.4	⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
mplvrpmga.5	⊢ (𝜑 → 𝐼 ∈ 𝑉)

Assertion

Ref	Expression
mplvrpmga	⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))

Distinct variable groups:   𝐴,𝑑,𝑓,𝑥   𝐼,𝑑,𝑓,ℎ,𝑥   𝑀,𝑑,𝑓,𝑥   𝑃,𝑑,𝑓,𝑥   𝑥,𝑅   𝜑,𝑑,𝑓,𝑥

Allowed substitution hints:   𝜑(ℎ)   𝐴(ℎ)   𝑃(ℎ)   𝑅(𝑓, ℎ, 𝑑)   𝑆(𝑥, 𝑓, ℎ, 𝑑)   𝑀(ℎ)   𝑉(𝑥, 𝑓, ℎ, 𝑑)

Proof of Theorem mplvrpmga

Dummy variables 𝑔 𝑝 𝑞 𝑐 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mplvrpmga.5	. . 3 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
2		mplvrpmga.1	. . . 4 ⊢ 𝑆 = (SymGrp‘𝐼)
3	2	symggrp 19607	. . 3 ⊢ (𝐼 ∈ 𝑉 → 𝑆 ∈ Grp)
4	1, 3	syl 18	. 2 ⊢ (𝜑 → 𝑆 ∈ Grp)
5		mplvrpmga.3	. . . 4 ⊢ 𝑀 = (Base‘(𝐼 mPoly 𝑅))
6	5	fvexi 6897	. . 3 ⊢ 𝑀 ∈ V
7	6	a1i 11	. 2 ⊢ (𝜑 → 𝑀 ∈ V)
8		fvexd 6898	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (Base‘𝑅) ∈ V)
9		ovex 7451	. . . . . . . 8 ⊢ (ℕ0 ↑m 𝐼) ∈ V
10	9	rabex 5300	. . . . . . 7 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V
11	10	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
12		eqid 2761	. . . . . . . . 9 ⊢ (𝐼 mPoly 𝑅) = (𝐼 mPoly 𝑅)
13		eqid 2761	. . . . . . . . 9 ⊢ (Base‘𝑅) = (Base‘𝑅)
14		eqid 2761	. . . . . . . . . 10 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
15	14	psrbasfsupp 34136	. . . . . . . . 9 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
16		xp2nd 8032	. . . . . . . . . 10 ⊢ (𝑐 ∈ (𝑃 × 𝑀) → (2nd ‘𝑐) ∈ 𝑀)
17	16	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (2nd ‘𝑐) ∈ 𝑀)
18	12, 13, 5, 15, 17	mplelf 22298	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (2nd ‘𝑐):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
19		mplvrpmga.2	. . . . . . . . 9 ⊢ 𝑃 = (Base‘𝑆)
20	1	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
21		xp1st 8031	. . . . . . . . . 10 ⊢ (𝑐 ∈ (𝑃 × 𝑀) → (1st ‘𝑐) ∈ 𝑃)
22	21	ad2antlr 740	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (1st ‘𝑐) ∈ 𝑃)
23		simpr 490	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
24	2, 19, 20, 22, 23	mplvrpmlem 34168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ (1st ‘𝑐)) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
25	18, 24	ffvelcdmd 7083	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐))) ∈ (Base‘𝑅))
26	25	fmpttd 7113	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
27	8, 11, 26	elmapdd 8854	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) ∈ ((Base‘𝑅) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}))
28		eqid 2761	. . . . . . 7 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
29		eqid 2761	. . . . . . 7 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
30	28, 13, 15, 29, 1	psrbas 22235	. . . . . 6 ⊢ (𝜑 → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}))
31	30	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}))
32	27, 31	eleqtrrd 2864	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) ∈ (Base‘(𝐼 mPwSer 𝑅)))
33		coeq1 5835	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∘ (1st ‘𝑐)) = (𝑦 ∘ (1st ‘𝑐)))
34	33	fveq2d 6887	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐))) = ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐))))
35	34	cbvmptv 5209	. . . . 5 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐))))
36		fveq1 6882	. . . . . . . 8 ⊢ (𝑔 = (2nd ‘𝑐) → (𝑔‘(𝑦 ∘ 𝑞)) = ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞)))
37	36	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑔 = (2nd ‘𝑐) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞))))
38	37	breq1d 5113	. . . . . 6 ⊢ (𝑔 = (2nd ‘𝑐) → ((𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅) ↔ (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅)))
39		coeq2 5836	. . . . . . . . 9 ⊢ (𝑞 = (1st ‘𝑐) → (𝑦 ∘ 𝑞) = (𝑦 ∘ (1st ‘𝑐)))
40	39	fveq2d 6887	. . . . . . . 8 ⊢ (𝑞 = (1st ‘𝑐) → ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞)) = ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐))))
41	40	mpteq2dv 5199	. . . . . . 7 ⊢ (𝑞 = (1st ‘𝑐) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞))) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐)))))
42	41	breq1d 5113	. . . . . 6 ⊢ (𝑞 = (1st ‘𝑐) → ((𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅) ↔ (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐)))) finSupp (0g‘𝑅)))
43		mplvrpmga.4	. . . . . . . . . . . . 13 ⊢ 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
44	43	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
45		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝑞 ∧ 𝑓 = 𝑔) → 𝑓 = 𝑔)
46		coeq2 5836	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑞 → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝑞))
47	46	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 = 𝑞 ∧ 𝑓 = 𝑔) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝑞))
48	45, 47	fveq12d 6890	. . . . . . . . . . . . . 14 ⊢ ((𝑑 = 𝑞 ∧ 𝑓 = 𝑔) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑔‘(𝑥 ∘ 𝑞)))
49	48	mpteq2dv 5199	. . . . . . . . . . . . 13 ⊢ ((𝑑 = 𝑞 ∧ 𝑓 = 𝑔) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))))
50	49	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) ∧ (𝑑 = 𝑞 ∧ 𝑓 = 𝑔)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))))
51		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → 𝑞 ∈ 𝑃)
52		simplr 781	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → 𝑔 ∈ 𝑀)
53	10	mptex 7227	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))) ∈ V
54	53	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))) ∈ V)
55	44, 50, 51, 52, 54	ovmpod 7570	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → (𝑞𝐴𝑔) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))))
56		coeq1 5835	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∘ 𝑞) = (𝑦 ∘ 𝑞))
57	56	fveq2d 6887	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑔‘(𝑥 ∘ 𝑞)) = (𝑔‘(𝑦 ∘ 𝑞)))
58	57	cbvmptv 5209	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ 𝑞))) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))
59	55, 58	eqtrdi 2812	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → (𝑞𝐴𝑔) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))))
60	1	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → 𝐼 ∈ 𝑉)
61		eqid 2761	. . . . . . . . . . 11 ⊢ (0g‘𝑅) = (0g‘𝑅)
62	2, 19, 5, 43, 60, 61, 52, 51	mplvrpmfgalem 34169	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → (𝑞𝐴𝑔) finSupp (0g‘𝑅))
63	59, 62	eqbrtrrd 5129	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅))
64	63	anasss 472	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝑀 ∧ 𝑞 ∈ 𝑃)) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅))
65	64	ralrimivva 3206	. . . . . . 7 ⊢ (𝜑 → ∀𝑔 ∈ 𝑀 ∀𝑞 ∈ 𝑃 (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅))
66	65	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → ∀𝑔 ∈ 𝑀 ∀𝑞 ∈ 𝑃 (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅))
67	16	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (2nd ‘𝑐) ∈ 𝑀)
68	21	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (1st ‘𝑐) ∈ 𝑃)
69	38, 42, 66, 67, 68	rspc2dv 3591	. . . . 5 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑦 ∘ (1st ‘𝑐)))) finSupp (0g‘𝑅))
70	35, 69	eqbrtrid 5140	. . . 4 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) finSupp (0g‘𝑅))
71	12, 28, 29, 61, 5	mplelbas 22291	. . . 4 ⊢ ((𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) ∈ 𝑀 ↔ ((𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) finSupp (0g‘𝑅)))
72	32, 70, 71	sylanbrc 595	. . 3 ⊢ ((𝜑 ∧ 𝑐 ∈ (𝑃 × 𝑀)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) ∈ 𝑀)
73		vex 3455	. . . . . . . 8 ⊢ 𝑑 ∈ V
74		vex 3455	. . . . . . . 8 ⊢ 𝑓 ∈ V
75	73, 74	op2ndd 8010	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑓⟩ → (2nd ‘𝑐) = 𝑓)
76	73, 74	op1std 8009	. . . . . . . 8 ⊢ (𝑐 = ⟨𝑑, 𝑓⟩ → (1st ‘𝑐) = 𝑑)
77	76	coeq2d 5840	. . . . . . 7 ⊢ (𝑐 = ⟨𝑑, 𝑓⟩ → (𝑥 ∘ (1st ‘𝑐)) = (𝑥 ∘ 𝑑))
78	75, 77	fveq12d 6890	. . . . . 6 ⊢ (𝑐 = ⟨𝑑, 𝑓⟩ → ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐))) = (𝑓‘(𝑥 ∘ 𝑑)))
79	78	mpteq2dv 5199	. . . . 5 ⊢ (𝑐 = ⟨𝑑, 𝑓⟩ → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
80	79	mpompt 7532	. . . 4 ⊢ (𝑐 ∈ (𝑃 × 𝑀) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐))))) = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))))
81	43, 80	eqtr4i 2787	. . 3 ⊢ 𝐴 = (𝑐 ∈ (𝑃 × 𝑀) ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ ((2nd ‘𝑐)‘(𝑥 ∘ (1st ‘𝑐)))))
82	72, 81	fmptd 7112	. 2 ⊢ (𝜑 → 𝐴:(𝑃 × 𝑀)⟶𝑀)
83	2	symgid 19608	. . . . . . . 8 ⊢ (𝐼 ∈ 𝑉 → ( I ↾ 𝐼) = (0g‘𝑆))
84	1, 83	syl 18	. . . . . . 7 ⊢ (𝜑 → ( I ↾ 𝐼) = (0g‘𝑆))
85	84	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → ( I ↾ 𝐼) = (0g‘𝑆))
86	85	oveq1d 7433	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → (( I ↾ 𝐼)𝐴𝑔) = ((0g‘𝑆)𝐴𝑔))
87	43	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
88		ssrab2 4028	. . . . . . . . . . . . . 14 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼)
89	88	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
90	89	sselda 3931	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ0 ↑m 𝐼))
91	90	elmaprd 8863	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
92		fcoi1 6754	. . . . . . . . . . 11 ⊢ (𝑥:𝐼⟶ℕ0 → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
93	91, 92	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ ( I ↾ 𝐼)) = 𝑥)
94	93	fveq2d 6887	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑔‘(𝑥 ∘ ( I ↾ 𝐼))) = (𝑔‘𝑥))
95	94	mpteq2dva 5198	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ ( I ↾ 𝐼)))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘𝑥)))
96	95	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ (𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ ( I ↾ 𝐼)))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘𝑥)))
97		simpr 490	. . . . . . . . . 10 ⊢ ((𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔) → 𝑓 = 𝑔)
98		coeq2 5836	. . . . . . . . . . 11 ⊢ (𝑑 = ( I ↾ 𝐼) → (𝑥 ∘ 𝑑) = (𝑥 ∘ ( I ↾ 𝐼)))
99	98	adantr 486	. . . . . . . . . 10 ⊢ ((𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔) → (𝑥 ∘ 𝑑) = (𝑥 ∘ ( I ↾ 𝐼)))
100	97, 99	fveq12d 6890	. . . . . . . . 9 ⊢ ((𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑔‘(𝑥 ∘ ( I ↾ 𝐼))))
101	100	mpteq2dv 5199	. . . . . . . 8 ⊢ ((𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ ( I ↾ 𝐼)))))
102	101	adantl 487	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ (𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ ( I ↾ 𝐼)))))
103	12, 28, 29, 61, 5	mplelbas 22291	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝑀 ↔ (𝑔 ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ 𝑔 finSupp (0g‘𝑅)))
104	103	simplbi 502	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑀 → 𝑔 ∈ (Base‘(𝐼 mPwSer 𝑅)))
105	28, 13, 15, 29, 104	psrelbas 22236	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝑀 → 𝑔:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
106	105	ad3antlr 744	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑑 = ( I ↾ 𝐼)) ∧ 𝑓 = 𝑔) → 𝑔:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
107	106	feqmptd 6951	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑑 = ( I ↾ 𝐼)) ∧ 𝑓 = 𝑔) → 𝑔 = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘𝑥)))
108	107	anasss 472	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ (𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔)) → 𝑔 = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘𝑥)))
109	96, 102, 108	3eqtr4d 2806	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ (𝑑 = ( I ↾ 𝐼) ∧ 𝑓 = 𝑔)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = 𝑔)
110		eqid 2761	. . . . . . . . . 10 ⊢ (0g‘𝑆) = (0g‘𝑆)
111	19, 110	grpidcl 19169	. . . . . . . . 9 ⊢ (𝑆 ∈ Grp → (0g‘𝑆) ∈ 𝑃)
112	1, 3, 111	3syl 19	. . . . . . . 8 ⊢ (𝜑 → (0g‘𝑆) ∈ 𝑃)
113	84, 112	eqeltrd 2861	. . . . . . 7 ⊢ (𝜑 → ( I ↾ 𝐼) ∈ 𝑃)
114	113	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → ( I ↾ 𝐼) ∈ 𝑃)
115		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → 𝑔 ∈ 𝑀)
116	87, 109, 114, 115, 115	ovmpod 7570	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → (( I ↾ 𝐼)𝐴𝑔) = 𝑔)
117	86, 116	eqtr3d 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → ((0g‘𝑆)𝐴𝑔) = 𝑔)
118		eqid 2761	. . . . . . . . . 10 ⊢ (+g‘𝑆) = (+g‘𝑆)
119	2, 19, 118	symgov 19591	. . . . . . . . 9 ⊢ ((𝑝 ∈ 𝑃 ∧ 𝑞 ∈ 𝑃) → (𝑝(+g‘𝑆)𝑞) = (𝑝 ∘ 𝑞))
120	119	adantll 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝(+g‘𝑆)𝑞) = (𝑝 ∘ 𝑞))
121	120	oveq1d 7433	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = ((𝑝 ∘ 𝑞)𝐴𝑔))
122		coass 6266	. . . . . . . . . . 11 ⊢ ((𝑥 ∘ 𝑝) ∘ 𝑞) = (𝑥 ∘ (𝑝 ∘ 𝑞))
123	122	a1i 11	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ((𝑥 ∘ 𝑝) ∘ 𝑞) = (𝑥 ∘ (𝑝 ∘ 𝑞)))
124	123	fveq2d 6887	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞)) = (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞))))
125	124	mpteq2dva 5198	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞)))))
126	59	adantlr 728	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑞𝐴𝑔) = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))))
127	126	oveq2d 7434	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝𝐴(𝑞𝐴𝑔)) = (𝑝𝐴(𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))))
128	43	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝐴 = (𝑑 ∈ 𝑃, 𝑓 ∈ 𝑀 ↦ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑)))))
129		simpllr 788	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑑 = 𝑝)
130	129	coeq2d 5840	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑑) = (𝑥 ∘ 𝑝))
131	130	fveq2d 6887	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑓‘(𝑥 ∘ 𝑝)))
132		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))))
133		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝑝)) → 𝑦 = (𝑥 ∘ 𝑝))
134	133	coeq1d 5839	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝑝)) → (𝑦 ∘ 𝑞) = ((𝑥 ∘ 𝑝) ∘ 𝑞))
135	134	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) ∧ 𝑦 = (𝑥 ∘ 𝑝)) → (𝑔‘(𝑦 ∘ 𝑞)) = (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞)))
136		breq1 5106	. . . . . . . . . . . . . . 15 ⊢ (ℎ = (𝑥 ∘ 𝑝) → (ℎ finSupp 0 ↔ (𝑥 ∘ 𝑝) finSupp 0))
137		nn0ex 12605	. . . . . . . . . . . . . . . . 17 ⊢ ℕ0 ∈ V
138	137	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
139	1	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝐼 ∈ 𝑉)
140	139	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
141	88	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
142	141	sselda 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ (ℕ0 ↑m 𝐼))
143	142	elmaprd 8863	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥:𝐼⟶ℕ0)
144	2, 19	symgbasf 19583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑃 → 𝑝:𝐼⟶𝐼)
145	144	ad5antlr 748	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝:𝐼⟶𝐼)
146	143, 145	fcod 6733	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑝):𝐼⟶ℕ0)
147	138, 140, 146	elmapdd 8854	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑝) ∈ (ℕ0 ↑m 𝐼))
148		breq1 5106	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ = 𝑥 → (ℎ finSupp 0 ↔ 𝑥 finSupp 0))
149	148	elrab 3645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↔ (𝑥 ∈ (ℕ0 ↑m 𝐼) ∧ 𝑥 finSupp 0))
150	149	simprbi 503	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} → 𝑥 finSupp 0)
151	150	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 finSupp 0)
152	2, 19	symgbasf1o 19582	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ 𝑃 → 𝑝:𝐼–1-1-onto→𝐼)
153		f1of1 6821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝:𝐼–1-1-onto→𝐼 → 𝑝:𝐼–1-1→𝐼)
154	152, 153	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ 𝑃 → 𝑝:𝐼–1-1→𝐼)
155	154	ad5antlr 748	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑝:𝐼–1-1→𝐼)
156		0nn0 12614	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ ℕ0
157	156	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 0 ∈ ℕ0)
158		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
159	151, 155, 157, 158	fsuppco 9387	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑝) finSupp 0)
160	136, 147, 159	elrabd 3647	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑥 ∘ 𝑝) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
161		fvexd 6898	. . . . . . . . . . . . . 14 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞)) ∈ V)
162		nfv 1947	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝)
163		nfmpt1 5204	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦(𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))
164	163	nfeq2 2940	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑦 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))
165	162, 164	nfan 1932	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦(((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))))
166		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}
167	165, 166	nfan 1932	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
168		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑥 ∘ 𝑝)
169		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))
170	132, 135, 160, 161, 167, 168, 169	fvmptdf 6998	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑝)) = (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞)))
171	131, 170	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) ∧ 𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞)))
172	171	mpteq2dva 5198	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑑 = 𝑝) ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))))
173	172	anasss 472	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ (𝑑 = 𝑝 ∧ 𝑓 = (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))))) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))))
174		simplr 781	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝑝 ∈ 𝑃)
175		fvexd 6898	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (Base‘𝑅) ∈ V)
176	10	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ∈ V)
177	115	ad3antrrr 743	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑔 ∈ 𝑀)
178	12, 13, 5, 15, 177	mplelf 22298	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑔:{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
179		breq1 5106	. . . . . . . . . . . . . . . 16 ⊢ (ℎ = (𝑦 ∘ 𝑞) → (ℎ finSupp 0 ↔ (𝑦 ∘ 𝑞) finSupp 0))
180	137	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → ℕ0 ∈ V)
181	139	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝐼 ∈ 𝑉)
182	88	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ⊆ (ℕ0 ↑m 𝐼))
183	182	sselda 3931	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑦 ∈ (ℕ0 ↑m 𝐼))
184	183	elmaprd 8863	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑦:𝐼⟶ℕ0)
185	2, 19	symgbasf 19583	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ 𝑃 → 𝑞:𝐼⟶𝐼)
186	185	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑞:𝐼⟶𝐼)
187	184, 186	fcod 6733	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∘ 𝑞):𝐼⟶ℕ0)
188	180, 181, 187	elmapdd 8854	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∘ 𝑞) ∈ (ℕ0 ↑m 𝐼))
189		breq1 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑦 → (ℎ finSupp 0 ↔ 𝑦 finSupp 0))
190	189	elrab 3645	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↔ (𝑦 ∈ (ℕ0 ↑m 𝐼) ∧ 𝑦 finSupp 0))
191	190	simprbi 503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} → 𝑦 finSupp 0)
192	191	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑦 finSupp 0)
193	2, 19	symgbasf1o 19582	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ 𝑃 → 𝑞:𝐼–1-1-onto→𝐼)
194	193	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑞:𝐼–1-1-onto→𝐼)
195		f1of1 6821	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞:𝐼–1-1-onto→𝐼 → 𝑞:𝐼–1-1→𝐼)
196	194, 195	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑞:𝐼–1-1→𝐼)
197	156	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 0 ∈ ℕ0)
198		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
199	192, 196, 197, 198	fsuppco 9387	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∘ 𝑞) finSupp 0)
200	179, 188, 199	elrabd 3647	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑦 ∘ 𝑞) ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0})
201	178, 200	ffvelcdmd 7083	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ 𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}) → (𝑔‘(𝑦 ∘ 𝑞)) ∈ (Base‘𝑅))
202	201	fmpttd 7113	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))):{ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}⟶(Base‘𝑅))
203	175, 176, 202	elmapdd 8854	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) ∈ ((Base‘𝑅) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}))
204	30	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (Base‘(𝐼 mPwSer 𝑅)) = ((Base‘𝑅) ↑m {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0}))
205	203, 204	eleqtrrd 2864	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) ∈ (Base‘(𝐼 mPwSer 𝑅)))
206	63	adantlr 728	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅))
207	12, 28, 29, 61, 5	mplelbas 22291	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) ∈ 𝑀 ↔ ((𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) ∈ (Base‘(𝐼 mPwSer 𝑅)) ∧ (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) finSupp (0g‘𝑅)))
208	205, 206, 207	sylanbrc 595	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞))) ∈ 𝑀)
209	176	mptexd 7228	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))) ∈ V)
210	128, 173, 174, 208, 209	ovmpod 7570	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝𝐴(𝑦 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑦 ∘ 𝑞)))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))))
211	127, 210	eqtrd 2796	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝𝐴(𝑞𝐴𝑔)) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘((𝑥 ∘ 𝑝) ∘ 𝑞))))
212		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑑 = (𝑝 ∘ 𝑞) ∧ 𝑓 = 𝑔) → 𝑓 = 𝑔)
213		coeq2 5836	. . . . . . . . . . . . 13 ⊢ (𝑑 = (𝑝 ∘ 𝑞) → (𝑥 ∘ 𝑑) = (𝑥 ∘ (𝑝 ∘ 𝑞)))
214	213	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑑 = (𝑝 ∘ 𝑞) ∧ 𝑓 = 𝑔) → (𝑥 ∘ 𝑑) = (𝑥 ∘ (𝑝 ∘ 𝑞)))
215	212, 214	fveq12d 6890	. . . . . . . . . . 11 ⊢ ((𝑑 = (𝑝 ∘ 𝑞) ∧ 𝑓 = 𝑔) → (𝑓‘(𝑥 ∘ 𝑑)) = (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞))))
216	215	mpteq2dv 5199	. . . . . . . . . 10 ⊢ ((𝑑 = (𝑝 ∘ 𝑞) ∧ 𝑓 = 𝑔) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞)))))
217	216	adantl 487	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) ∧ (𝑑 = (𝑝 ∘ 𝑞) ∧ 𝑓 = 𝑔)) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑓‘(𝑥 ∘ 𝑑))) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞)))))
218	139, 3	syl 18	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝑆 ∈ Grp)
219		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝑞 ∈ 𝑃)
220	19, 118, 218, 174, 219	grpcld 19151	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝(+g‘𝑆)𝑞) ∈ 𝑃)
221	120, 220	eqeltrrd 2862	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑝 ∘ 𝑞) ∈ 𝑃)
222		simpllr 788	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → 𝑔 ∈ 𝑀)
223	176	mptexd 7228	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞)))) ∈ V)
224	128, 217, 221, 222, 223	ovmpod 7570	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → ((𝑝 ∘ 𝑞)𝐴𝑔) = (𝑥 ∈ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ ℎ finSupp 0} ↦ (𝑔‘(𝑥 ∘ (𝑝 ∘ 𝑞)))))
225	125, 211, 224	3eqtr4rd 2807	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → ((𝑝 ∘ 𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔)))
226	121, 225	eqtrd 2796	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ 𝑝 ∈ 𝑃) ∧ 𝑞 ∈ 𝑃) → ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔)))
227	226	anasss 472	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝑀) ∧ (𝑝 ∈ 𝑃 ∧ 𝑞 ∈ 𝑃)) → ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔)))
228	227	ralrimivva 3206	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → ∀𝑝 ∈ 𝑃 ∀𝑞 ∈ 𝑃 ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔)))
229	117, 228	jca 521	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝑀) → (((0g‘𝑆)𝐴𝑔) = 𝑔 ∧ ∀𝑝 ∈ 𝑃 ∀𝑞 ∈ 𝑃 ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔))))
230	229	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑔 ∈ 𝑀 (((0g‘𝑆)𝐴𝑔) = 𝑔 ∧ ∀𝑝 ∈ 𝑃 ∀𝑞 ∈ 𝑃 ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔))))
231	19, 118, 110	isga 19498	. 2 ⊢ (𝐴 ∈ (𝑆 GrpAct 𝑀) ↔ ((𝑆 ∈ Grp ∧ 𝑀 ∈ V) ∧ (𝐴:(𝑃 × 𝑀)⟶𝑀 ∧ ∀𝑔 ∈ 𝑀 (((0g‘𝑆)𝐴𝑔) = 𝑔 ∧ ∀𝑝 ∈ 𝑃 ∀𝑞 ∈ 𝑃 ((𝑝(+g‘𝑆)𝑞)𝐴𝑔) = (𝑝𝐴(𝑞𝐴𝑔))))))
232	4, 7, 82, 230, 231	syl22anbrc 33049	1 ⊢ (𝜑 → 𝐴 ∈ (𝑆 GrpAct 𝑀))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  {crab 3413  Vcvv 3451   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103   ↦ cmpt 5186   I cid 5545   × cxp 5649   ↾ cres 5653   ∘ ccom 5655  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418   ∈ cmpo 7420  1^st c1st 7997  2^nd c2nd 7998   ↑_m cmap 8840   finSupp cfsupp 9346  0cc0 11193  ℕ₀cn0 12599  Basecbs 17380  +_gcplusg 17421  0_gc0g 17603  Grpcgrp 19137   GrpAct cga 19496  SymGrpcsymg 19576   mPwSer cmps 22205   mPoly cmpl 22207

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-om 7876  df-1st 7999  df-2nd 8000  df-supp 8171  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-er 8710  df-map 8842  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-fsupp 9347  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-3 12399  df-4 12400  df-5 12401  df-6 12402  df-7 12403  df-8 12404  df-9 12405  df-n0 12600  df-z 12687  df-uz 12959  df-fz 13633  df-struct 17318  df-sets 17335  df-slot 17353  df-ndx 17365  df-base 17381  df-ress 17402  df-plusg 17434  df-mulr 17435  df-sca 17437  df-vsca 17438  df-tset 17440  df-0g 17605  df-mgm 18809  df-sgrp 18901  df-mnd 18917  df-submnd 18972  df-efmnd 19058  df-grp 19140  df-ga 19497  df-symg 19577  df-psr 22210  df-mpl 22212

This theorem is used by:  mplvrpmmhm  34171  mplvrpmrhm  34172  splysubrg  34185  issply  34186