This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplvrpmmhm

Description: The action of permuting variables in a multivariate polynomial is a monoid homomorphism. (Contributed by Thierry Arnoux, 11-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 )
mplvrpmmhm.f 
|- F = ( f e. M |-> ( D A f ) )
mplvrpmmhm.w 
|- W = ( I mPoly R )
mplvrpmmhm.1 
|- ( ph -> R e. Ring )
mplvrpmmhm.2 
|- ( ph -> D e. P )
Assertion mplvrpmmhm 
|- ( ph -> F e. ( W MndHom W ) )

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 mplvrpmmhm.f 
 |-  F = ( f e. M |-> ( D A f ) )
7 mplvrpmmhm.w 
 |-  W = ( I mPoly R )
8 mplvrpmmhm.1 
 |-  ( ph -> R e. Ring )
9 mplvrpmmhm.2 
 |-  ( ph -> D e. P )
10 7 fveq2i 
 |-  ( Base ` W ) = ( Base ` ( I mPoly R ) )
11 3 10 eqtr4i 
 |-  M = ( Base ` W )
12 eqid 
 |-  ( +g ` W ) = ( +g ` W )
13 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
14 7 5 8 mplringd 
 |-  ( ph -> W e. Ring )
15 14 ringgrpd 
 |-  ( ph -> W e. Grp )
16 15 grpmndd 
 |-  ( ph -> W e. Mnd )
17 1 2 3 4 5 mplvrpmga 
 |-  ( ph -> A e. ( S GrpAct M ) )
18 2 gaf 
 |-  ( A e. ( S GrpAct M ) -> A : ( P X. M ) --> M )
19 17 18 syl 
 |-  ( ph -> A : ( P X. M ) --> M )
20 19 fovcld 
 |-  ( ( ph /\ D e. P /\ f e. M ) -> ( D A f ) e. M )
21 20 3expa 
 |-  ( ( ( ph /\ D e. P ) /\ f e. M ) -> ( D A f ) e. M )
22 21 an32s 
 |-  ( ( ( ph /\ f e. M ) /\ D e. P ) -> ( D A f ) e. M )
23 9 22 mpidan 
 |-  ( ( ph /\ f e. M ) -> ( D A f ) e. M )
24 23 6 fmptd 
 |-  ( ph -> F : M --> M )
25 eqid 
 |-  ( Base ` R ) = ( Base ` R )
26 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
27 26 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
28 simplr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> i e. M )
29 7 25 11 27 28 mplelf 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> i : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
30 29 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
31 30 ffnd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i Fn { h e. ( NN0 ^m I ) | h finSupp 0 } )
32 simpr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> j e. M )
33 7 25 11 27 32 mplelf 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> j : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
34 33 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> j : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
35 34 ffnd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> j Fn { h e. ( NN0 ^m I ) | h finSupp 0 } )
36 ovex 
 |-  ( NN0 ^m I ) e. _V
37 36 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
38 37 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
39 breq1 
 |-  ( h = ( x o. D ) -> ( h finSupp 0 <-> ( x o. D ) finSupp 0 ) )
40 nn0ex 
 |-  NN0 e. _V
41 40 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
42 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
43 5 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
44 40 a1i 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
45 breq1 
 |-  ( h = x -> ( h finSupp 0 <-> x finSupp 0 ) )
46 45 elrab 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } <-> ( x e. ( NN0 ^m I ) /\ x finSupp 0 ) )
47 46 biimpi 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> ( x e. ( NN0 ^m I ) /\ x finSupp 0 ) )
48 47 adantl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x e. ( NN0 ^m I ) /\ x finSupp 0 ) )
49 48 simpld 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. ( NN0 ^m I ) )
50 43 44 49 elmaprd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x : I --> NN0 )
51 50 ad4ant14 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x : I --> NN0 )
52 1 2 symgbasf1o 
 |-  ( D e. P -> D : I -1-1-onto-> I )
53 9 52 syl 
 |-  ( ph -> D : I -1-1-onto-> I )
54 f1of 
 |-  ( D : I -1-1-onto-> I -> D : I --> I )
55 53 54 syl 
 |-  ( ph -> D : I --> I )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D : I --> I )
57 51 56 fcod 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) : I --> NN0 )
58 41 42 57 elmapdd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) e. ( NN0 ^m I ) )
59 48 simprd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x finSupp 0 )
60 53 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D : I -1-1-onto-> I )
61 f1of1 
 |-  ( D : I -1-1-onto-> I -> D : I -1-1-> I )
62 60 61 syl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D : I -1-1-> I )
63 0nn0 
 |-  0 e. NN0
64 63 a1i 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> 0 e. NN0 )
65 simpr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
66 59 62 64 65 fsuppco 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) finSupp 0 )
67 66 ad4ant14 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) finSupp 0 )
68 39 58 67 elrabd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
69 fnfvof 
 |-  ( ( ( i Fn { h e. ( NN0 ^m I ) | h finSupp 0 } /\ j Fn { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V /\ ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) ) -> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) = ( ( i ` ( x o. D ) ) ( +g ` R ) ( j ` ( x o. D ) ) ) )
70 31 35 38 68 69 syl22anc 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) = ( ( i ` ( x o. D ) ) ( +g ` R ) ( j ` ( x o. D ) ) ) )
71 oveq2 
 |-  ( f = i -> ( D A f ) = ( D A i ) )
72 4 a1i 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
73 simpr 
 |-  ( ( d = D /\ f = i ) -> f = i )
74 coeq2 
 |-  ( d = D -> ( x o. d ) = ( x o. D ) )
75 74 adantr 
 |-  ( ( d = D /\ f = i ) -> ( x o. d ) = ( x o. D ) )
76 73 75 fveq12d 
 |-  ( ( d = D /\ f = i ) -> ( f ` ( x o. d ) ) = ( i ` ( x o. D ) ) )
77 76 mpteq2dv 
 |-  ( ( d = D /\ f = i ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) )
78 77 adantl 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = i ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) )
79 9 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> D e. P )
80 37 a1i 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
81 80 mptexd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) e. _V )
82 72 78 79 28 81 ovmpod 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( D A i ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) )
83 71 82 sylan9eqr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ f = i ) -> ( D A f ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) )
84 6 83 28 81 fvmptd2 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` i ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) )
85 fvexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( i ` ( x o. D ) ) e. _V )
86 84 85 fvmpt2d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( F ` i ) ` x ) = ( i ` ( x o. D ) ) )
87 oveq2 
 |-  ( f = j -> ( D A f ) = ( D A j ) )
88 simpr 
 |-  ( ( d = D /\ f = j ) -> f = j )
89 74 adantr 
 |-  ( ( d = D /\ f = j ) -> ( x o. d ) = ( x o. D ) )
90 88 89 fveq12d 
 |-  ( ( d = D /\ f = j ) -> ( f ` ( x o. d ) ) = ( j ` ( x o. D ) ) )
91 90 mpteq2dv 
 |-  ( ( d = D /\ f = j ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) )
92 91 adantl 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = j ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) )
93 80 mptexd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) e. _V )
94 72 92 79 32 93 ovmpod 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( D A j ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) )
95 87 94 sylan9eqr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ f = j ) -> ( D A f ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) )
96 6 95 32 93 fvmptd2 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` j ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) )
97 fvexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( j ` ( x o. D ) ) e. _V )
98 96 97 fvmpt2d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( F ` j ) ` x ) = ( j ` ( x o. D ) ) )
99 86 98 oveq12d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( ( F ` i ) ` x ) ( +g ` R ) ( ( F ` j ) ` x ) ) = ( ( i ` ( x o. D ) ) ( +g ` R ) ( j ` ( x o. D ) ) ) )
100 70 99 eqtr4d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) = ( ( ( F ` i ) ` x ) ( +g ` R ) ( ( F ` j ) ` x ) ) )
101 100 mpteq2dva 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( F ` i ) ` x ) ( +g ` R ) ( ( F ` j ) ` x ) ) ) )
102 24 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> F : M --> M )
103 102 28 ffvelcdmd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` i ) e. M )
104 7 25 11 27 103 mplelf 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` i ) : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
105 104 ffnd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` i ) Fn { h e. ( NN0 ^m I ) | h finSupp 0 } )
106 102 32 ffvelcdmd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` j ) e. M )
107 7 25 11 27 106 mplelf 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` j ) : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
108 107 ffnd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` j ) Fn { h e. ( NN0 ^m I ) | h finSupp 0 } )
109 80 105 108 offvalfv 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( ( F ` i ) oF ( +g ` R ) ( F ` j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( ( F ` i ) ` x ) ( +g ` R ) ( ( F ` j ) ` x ) ) ) )
110 101 109 eqtr4d 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) ) = ( ( F ` i ) oF ( +g ` R ) ( F ` j ) ) )
111 oveq2 
 |-  ( f = ( i ( +g ` W ) j ) -> ( D A f ) = ( D A ( i ( +g ` W ) j ) ) )
112 simpr 
 |-  ( ( d = D /\ f = ( i ( +g ` W ) j ) ) -> f = ( i ( +g ` W ) j ) )
113 74 adantr 
 |-  ( ( d = D /\ f = ( i ( +g ` W ) j ) ) -> ( x o. d ) = ( x o. D ) )
114 112 113 fveq12d 
 |-  ( ( d = D /\ f = ( i ( +g ` W ) j ) ) -> ( f ` ( x o. d ) ) = ( ( i ( +g ` W ) j ) ` ( x o. D ) ) )
115 114 mpteq2dv 
 |-  ( ( d = D /\ f = ( i ( +g ` W ) j ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) )
116 115 adantl 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( +g ` W ) j ) ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) )
117 15 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> W e. Grp )
118 11 12 117 28 32 grpcld 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( i ( +g ` W ) j ) e. M )
119 80 mptexd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) e. _V )
120 72 116 79 118 119 ovmpod 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( D A ( i ( +g ` W ) j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) )
121 111 120 sylan9eqr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ f = ( i ( +g ` W ) j ) ) -> ( D A f ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) )
122 6 121 118 119 fvmptd2 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( +g ` W ) j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) )
123 eqid 
 |-  ( +g ` R ) = ( +g ` R )
124 7 11 123 12 28 32 mpladd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( i ( +g ` W ) j ) = ( i oF ( +g ` R ) j ) )
125 124 fveq1d 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) = ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) )
126 125 mpteq2dv 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i ( +g ` W ) j ) ` ( x o. D ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) ) )
127 122 126 eqtrd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( +g ` W ) j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( i oF ( +g ` R ) j ) ` ( x o. D ) ) ) )
128 7 11 123 12 103 106 mpladd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( ( F ` i ) ( +g ` W ) ( F ` j ) ) = ( ( F ` i ) oF ( +g ` R ) ( F ` j ) ) )
129 110 127 128 3eqtr4d 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( +g ` W ) j ) ) = ( ( F ` i ) ( +g ` W ) ( F ` j ) ) )
130 129 anasss 
 |-  ( ( ph /\ ( i e. M /\ j e. M ) ) -> ( F ` ( i ( +g ` W ) j ) ) = ( ( F ` i ) ( +g ` W ) ( F ` j ) ) )
131 simpr 
 |-  ( ( ph /\ f = ( 0g ` W ) ) -> f = ( 0g ` W ) )
132 131 oveq2d 
 |-  ( ( ph /\ f = ( 0g ` W ) ) -> ( D A f ) = ( D A ( 0g ` W ) ) )
133 4 a1i 
 |-  ( ph -> A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
134 simplrr 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f = ( 0g ` W ) )
135 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
136 8 ringgrpd 
 |-  ( ph -> R e. Grp )
137 7 27 135 13 5 136 mpl0 
 |-  ( ph -> ( 0g ` W ) = ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) )
138 137 ad2antrr 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 0g ` W ) = ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) )
139 134 138 eqtrd 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f = ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) )
140 74 ad2antrl 
 |-  ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) -> ( x o. d ) = ( x o. D ) )
141 140 adantr 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. d ) = ( x o. D ) )
142 139 141 fveq12d 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( f ` ( x o. d ) ) = ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) )
143 142 mpteq2dva 
 |-  ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) ) )
144 55 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D : I --> I )
145 50 144 fcod 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) : I --> NN0 )
146 44 43 145 elmapdd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) e. ( NN0 ^m I ) )
147 39 146 66 elrabd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
148 fvex 
 |-  ( 0g ` R ) e. _V
149 148 fvconst2 
 |-  ( ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) = ( 0g ` R ) )
150 147 149 syl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) = ( 0g ` R ) )
151 150 mpteq2dva 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( 0g ` R ) ) )
152 fconstmpt 
 |-  ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( 0g ` R ) )
153 137 152 eqtrdi 
 |-  ( ph -> ( 0g ` W ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( 0g ` R ) ) )
154 151 153 eqtr4d 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) ) = ( 0g ` W ) )
155 154 adantr 
 |-  ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( ( { h e. ( NN0 ^m I ) | h finSupp 0 } X. { ( 0g ` R ) } ) ` ( x o. D ) ) ) = ( 0g ` W ) )
156 143 155 eqtrd 
 |-  ( ( ph /\ ( d = D /\ f = ( 0g ` W ) ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( 0g ` W ) )
157 11 13 grpidcl 
 |-  ( W e. Grp -> ( 0g ` W ) e. M )
158 15 157 syl 
 |-  ( ph -> ( 0g ` W ) e. M )
159 133 156 9 158 158 ovmpod 
 |-  ( ph -> ( D A ( 0g ` W ) ) = ( 0g ` W ) )
160 159 adantr 
 |-  ( ( ph /\ f = ( 0g ` W ) ) -> ( D A ( 0g ` W ) ) = ( 0g ` W ) )
161 132 160 eqtrd 
 |-  ( ( ph /\ f = ( 0g ` W ) ) -> ( D A f ) = ( 0g ` W ) )
162 6 161 158 158 fvmptd2 
 |-  ( ph -> ( F ` ( 0g ` W ) ) = ( 0g ` W ) )
163 11 11 12 12 13 13 16 16 24 130 162 ismhmd 
 |-  ( ph -> F e. ( W MndHom W ) )