Metamath Proof Explorer

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