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