Metamath Proof Explorer

Theorem mplvrpmrhm

Description: The action of permuting variables in a multivariate polynomial is a ring homomorphism. (Contributed by Thierry Arnoux, 15-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 mplvrpmrhm 
|- ( ph -> F e. ( W RingHom 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 
 |-  ( 1r ` W ) = ( 1r ` W )
13 eqid 
 |-  ( .r ` W ) = ( .r ` W )
14 7 5 8 mplringd 
 |-  ( ph -> W e. Ring )
15 oveq2 
 |-  ( f = ( 1r ` W ) -> ( D A f ) = ( D A ( 1r ` W ) ) )
16 4 a1i 
 |-  ( ph -> A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
17 simpr 
 |-  ( ( d = D /\ f = ( 1r ` W ) ) -> f = ( 1r ` W ) )
18 simpl 
 |-  ( ( d = D /\ f = ( 1r ` W ) ) -> d = D )
19 18 coeq2d 
 |-  ( ( d = D /\ f = ( 1r ` W ) ) -> ( x o. d ) = ( x o. D ) )
20 17 19 fveq12d 
 |-  ( ( d = D /\ f = ( 1r ` W ) ) -> ( f ` ( x o. d ) ) = ( ( 1r ` W ) ` ( x o. D ) ) )
21 20 ad2antlr 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 1r ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( f ` ( x o. d ) ) = ( ( 1r ` W ) ` ( x o. D ) ) )
22 eqid 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | h finSupp 0 }
23 22 psrbasfsupp 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
26 7 23 24 25 12 5 8 mpl1 
 |-  ( ph -> ( 1r ` W ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 1r ` W ) = ( y e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
28 eqeq1 
 |-  ( y = ( x o. D ) -> ( y = ( I X. { 0 } ) <-> ( x o. D ) = ( I X. { 0 } ) ) )
29 9 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D e. P )
30 1 2 symgbasf1o 
 |-  ( D e. P -> D : I -1-1-onto-> I )
31 f1ococnv2 
 |-  ( D : I -1-1-onto-> I -> ( D o. `' D ) = ( _I |` I ) )
32 29 30 31 3syl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( D o. `' D ) = ( _I |` I ) )
33 32 adantr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( D o. `' D ) = ( _I |` I ) )
34 33 coeq2d 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( x o. ( D o. `' D ) ) = ( x o. ( _I |` I ) ) )
35 simpr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( x o. D ) = ( I X. { 0 } ) )
36 35 coeq1d 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( ( x o. D ) o. `' D ) = ( ( I X. { 0 } ) o. `' D ) )
37 coass 
 |-  ( ( x o. D ) o. `' D ) = ( x o. ( D o. `' D ) )
38 37 a1i 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( ( x o. D ) o. `' D ) = ( x o. ( D o. `' D ) ) )
39 9 30 syl 
 |-  ( ph -> D : I -1-1-onto-> I )
40 f1ocnv 
 |-  ( D : I -1-1-onto-> I -> `' D : I -1-1-onto-> I )
41 f1of 
 |-  ( `' D : I -1-1-onto-> I -> `' D : I --> I )
42 39 40 41 3syl 
 |-  ( ph -> `' D : I --> I )
43 0nn0 
 |-  0 e. NN0
44 43 a1i 
 |-  ( ph -> 0 e. NN0 )
45 42 44 constcof 
 |-  ( ph -> ( ( I X. { 0 } ) o. `' D ) = ( I X. { 0 } ) )
46 45 ad2antrr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( ( I X. { 0 } ) o. `' D ) = ( I X. { 0 } ) )
47 36 38 46 3eqtr3d 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( x o. ( D o. `' D ) ) = ( I X. { 0 } ) )
48 5 adantr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
49 nn0ex 
 |-  NN0 e. _V
50 49 a1i 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> NN0 e. _V )
51 ssrab2 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I )
52 simpr 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
53 51 52 sselid 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. ( NN0 ^m I ) )
54 48 50 53 elmaprd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x : I --> NN0 )
55 fcoi1 
 |-  ( x : I --> NN0 -> ( x o. ( _I |` I ) ) = x )
56 54 55 syl 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. ( _I |` I ) ) = x )
57 56 adantr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> ( x o. ( _I |` I ) ) = x )
58 34 47 57 3eqtr3rd 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ ( x o. D ) = ( I X. { 0 } ) ) -> x = ( I X. { 0 } ) )
59 simpr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x = ( I X. { 0 } ) ) -> x = ( I X. { 0 } ) )
60 59 coeq1d 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x = ( I X. { 0 } ) ) -> ( x o. D ) = ( ( I X. { 0 } ) o. D ) )
61 f1of 
 |-  ( D : I -1-1-onto-> I -> D : I --> I )
62 9 30 61 3syl 
 |-  ( ph -> D : I --> I )
63 62 44 constcof 
 |-  ( ph -> ( ( I X. { 0 } ) o. D ) = ( I X. { 0 } ) )
64 63 ad2antrr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x = ( I X. { 0 } ) ) -> ( ( I X. { 0 } ) o. D ) = ( I X. { 0 } ) )
65 60 64 eqtrd 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ x = ( I X. { 0 } ) ) -> ( x o. D ) = ( I X. { 0 } ) )
66 58 65 impbida 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( x o. D ) = ( I X. { 0 } ) <-> x = ( I X. { 0 } ) ) )
67 28 66 sylan9bbr 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y = ( x o. D ) ) -> ( y = ( I X. { 0 } ) <-> x = ( I X. { 0 } ) ) )
68 67 ifbid 
 |-  ( ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y = ( x o. D ) ) -> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
69 1 2 48 29 52 mplvrpmlem 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
70 fvexd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 1r ` R ) e. _V )
71 fvexd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 0g ` R ) e. _V )
72 70 71 ifcld 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
73 27 68 69 72 fvmptd 
 |-  ( ( ph /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( 1r ` W ) ` ( x o. D ) ) = if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
74 73 adantlr 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 1r ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( ( 1r ` W ) ` ( x o. D ) ) = if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
75 21 74 eqtrd 
 |-  ( ( ( ph /\ ( d = D /\ f = ( 1r ` W ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( f ` ( x o. d ) ) = if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
76 75 mpteq2dva 
 |-  ( ( ph /\ ( d = D /\ f = ( 1r ` 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 } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
77 11 12 14 ringidcld 
 |-  ( ph -> ( 1r ` W ) e. M )
78 ovex 
 |-  ( NN0 ^m I ) e. _V
79 78 rabex 
 |-  { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V
80 79 a1i 
 |-  ( ph -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
81 80 mptexd 
 |-  ( ph -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )
82 16 76 9 77 81 ovmpod 
 |-  ( ph -> ( D A ( 1r ` W ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
83 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
84 eqid 
 |-  ( 1r ` ( I mPwSer R ) ) = ( 1r ` ( I mPwSer R ) )
85 83 5 8 23 24 25 84 psr1 
 |-  ( ph -> ( 1r ` ( I mPwSer R ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
86 83 7 11 5 8 mplsubrg 
 |-  ( ph -> M e. ( SubRing ` ( I mPwSer R ) ) )
87 7 83 11 mplval2 
 |-  W = ( ( I mPwSer R ) |`s M )
88 87 84 subrg1 
 |-  ( M e. ( SubRing ` ( I mPwSer R ) ) -> ( 1r ` ( I mPwSer R ) ) = ( 1r ` W ) )
89 86 88 syl 
 |-  ( ph -> ( 1r ` ( I mPwSer R ) ) = ( 1r ` W ) )
90 82 85 89 3eqtr2d 
 |-  ( ph -> ( D A ( 1r ` W ) ) = ( 1r ` W ) )
91 15 90 sylan9eqr 
 |-  ( ( ph /\ f = ( 1r ` W ) ) -> ( D A f ) = ( 1r ` W ) )
92 6 91 77 77 fvmptd2 
 |-  ( ph -> ( F ` ( 1r ` W ) ) = ( 1r ` W ) )
93 nfcv 
 |-  F/_ v ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) )
94 eqid 
 |-  ( Base ` R ) = ( Base ` R )
95 fveq2 
 |-  ( v = ( y o. D ) -> ( i ` v ) = ( i ` ( y o. D ) ) )
96 oveq2 
 |-  ( v = ( y o. D ) -> ( ( x o. D ) oF - v ) = ( ( x o. D ) oF - ( y o. D ) ) )
97 96 fveq2d 
 |-  ( v = ( y o. D ) -> ( j ` ( ( x o. D ) oF - v ) ) = ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) )
98 95 97 oveq12d 
 |-  ( v = ( y o. D ) -> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) = ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) ) )
99 8 ringcmnd 
 |-  ( ph -> R e. CMnd )
100 99 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> R e. CMnd )
101 79 rabex 
 |-  { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } e. _V
102 101 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } e. _V )
103 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
104 7 83 11 103 mplbasss 
 |-  M C_ ( Base ` ( I mPwSer R ) )
105 simplr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> i e. M )
106 104 105 sselid 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> i e. ( Base ` ( I mPwSer R ) ) )
107 106 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i e. ( Base ` ( I mPwSer R ) ) )
108 83 94 23 103 107 psrelbas 
 |-  ( ( ( ( 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 ) )
109 108 feqmptd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i = ( v e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` v ) ) )
110 105 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i e. M )
111 7 11 24 110 mplelsfi 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> i finSupp ( 0g ` R ) )
112 109 111 eqbrtrrd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( v e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` v ) ) finSupp ( 0g ` R ) )
113 ssrab2 
 |-  { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } C_ { h e. ( NN0 ^m I ) | h finSupp 0 }
114 113 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } C_ { h e. ( NN0 ^m I ) | h finSupp 0 } )
115 fvexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( 0g ` R ) e. _V )
116 112 114 115 fmptssfisupp 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( i ` v ) ) finSupp ( 0g ` R ) )
117 eqid 
 |-  ( .r ` R ) = ( .r ` R )
118 8 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ n e. ( Base ` R ) ) -> R e. Ring )
119 simpr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ n e. ( Base ` R ) ) -> n e. ( Base ` R ) )
120 94 117 24 118 119 ringlzd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ n e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) n ) = ( 0g ` R ) )
121 108 adantr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> i : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
122 elrabi 
 |-  ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } -> v e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
123 122 adantl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
124 121 123 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( i ` v ) e. ( Base ` R ) )
125 simpr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> j e. M )
126 104 125 sselid 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> j e. ( Base ` ( I mPwSer R ) ) )
127 126 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> j e. ( Base ` ( I mPwSer R ) ) )
128 83 94 23 103 127 psrelbas 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> j : { h e. ( NN0 ^m I ) | h finSupp 0 } --> ( Base ` R ) )
129 69 ad5ant14 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
130 5 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> I e. V )
131 49 a1i 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> NN0 e. _V )
132 51 123 sselid 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v e. ( NN0 ^m I ) )
133 130 131 132 elmaprd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v : I --> NN0 )
134 breq1 
 |-  ( w = v -> ( w oR <_ ( x o. D ) <-> v oR <_ ( x o. D ) ) )
135 simpr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } )
136 134 135 elrabrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v oR <_ ( x o. D ) )
137 23 psrbagcon 
 |-  ( ( ( x o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } /\ v : I --> NN0 /\ v oR <_ ( x o. D ) ) -> ( ( ( x o. D ) oF - v ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } /\ ( ( x o. D ) oF - v ) oR <_ ( x o. D ) ) )
138 129 133 136 137 syl3anc 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( ( ( x o. D ) oF - v ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } /\ ( ( x o. D ) oF - v ) oR <_ ( x o. D ) ) )
139 138 simpld 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( ( x o. D ) oF - v ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
140 128 139 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( j ` ( ( x o. D ) oF - v ) ) e. ( Base ` R ) )
141 116 120 124 140 115 fsuppssov1 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) finSupp ( 0g ` R ) )
142 ssidd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( Base ` R ) C_ ( Base ` R ) )
143 8 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> R e. Ring )
144 94 117 143 124 140 ringcld 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) e. ( Base ` R ) )
145 breq1 
 |-  ( w = ( y o. D ) -> ( w oR <_ ( x o. D ) <-> ( y o. D ) oR <_ ( x o. D ) ) )
146 5 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> I e. V )
147 9 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> D e. P )
148 147 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> D e. P )
149 ssrab2 
 |-  { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } C_ { h e. ( NN0 ^m I ) | h finSupp 0 }
150 simpr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } )
151 149 150 sselid 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
152 151 adantlr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
153 1 2 146 148 152 mplvrpmlem 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( y o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
154 49 a1i 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> NN0 e. _V )
155 51 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 } C_ ( NN0 ^m I ) )
156 149 155 sstrid 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } C_ ( NN0 ^m I ) )
157 156 sselda 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y e. ( NN0 ^m I ) )
158 146 154 157 elmaprd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y : I --> NN0 )
159 158 ffnd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y Fn I )
160 54 ad4ant14 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x : I --> NN0 )
161 160 adantr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> x : I --> NN0 )
162 161 ffnd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> x Fn I )
163 62 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> D : I --> I )
164 breq1 
 |-  ( z = y -> ( z oR <_ x <-> y oR <_ x ) )
165 simpr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } )
166 164 165 elrabrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y oR <_ x )
167 159 162 163 146 146 166 ofrco 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( y o. D ) oR <_ ( x o. D ) )
168 145 153 167 elrabd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( y o. D ) e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } )
169 breq1 
 |-  ( z = ( v o. `' D ) -> ( z oR <_ x <-> ( v o. `' D ) oR <_ x ) )
170 breq1 
 |-  ( h = ( v o. `' D ) -> ( h finSupp 0 <-> ( v o. `' D ) finSupp 0 ) )
171 42 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> `' D : I --> I )
172 133 171 fcod 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) : I --> NN0 )
173 131 130 172 elmapdd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) e. ( NN0 ^m I ) )
174 breq1 
 |-  ( h = v -> ( h finSupp 0 <-> v finSupp 0 ) )
175 174 123 elrabrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v finSupp 0 )
176 39 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> D : I -1-1-onto-> I )
177 f1of1 
 |-  ( `' D : I -1-1-onto-> I -> `' D : I -1-1-> I )
178 176 40 177 3syl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> `' D : I -1-1-> I )
179 43 a1i 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> 0 e. NN0 )
180 175 178 179 123 fsuppco 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) finSupp 0 )
181 170 173 180 elrabd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
182 133 ffnd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> v Fn I )
183 160 adantr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> x : I --> NN0 )
184 183 ffnd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> x Fn I )
185 62 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> D : I --> I )
186 fnfco 
 |-  ( ( x Fn I /\ D : I --> I ) -> ( x o. D ) Fn I )
187 184 185 186 syl2anc 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( x o. D ) Fn I )
188 182 187 171 130 130 136 ofrco 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) oR <_ ( ( x o. D ) o. `' D ) )
189 176 31 syl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( D o. `' D ) = ( _I |` I ) )
190 189 coeq2d 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( x o. ( D o. `' D ) ) = ( x o. ( _I |` I ) ) )
191 183 55 syl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( x o. ( _I |` I ) ) = x )
192 190 191 eqtrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( x o. ( D o. `' D ) ) = x )
193 37 192 eqtrid 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( ( x o. D ) o. `' D ) = x )
194 188 193 breqtrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) oR <_ x )
195 169 181 194 elrabd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> ( v o. `' D ) e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } )
196 133 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> v : I --> NN0 )
197 158 adantlr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> y : I --> NN0 )
198 39 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> D : I -1-1-onto-> I )
199 196 197 198 cocnvf1o 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( v = ( y o. D ) <-> y = ( v o. `' D ) ) )
200 195 199 reu6dv 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } ) -> E! y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } v = ( y o. D ) )
201 93 94 24 98 100 102 141 142 144 168 200 gsummptfsf1o 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) = ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) ) ) ) )
202 coeq1 
 |-  ( t = y -> ( t o. D ) = ( y o. D ) )
203 202 fveq2d 
 |-  ( t = y -> ( i ` ( t o. D ) ) = ( i ` ( y o. D ) ) )
204 oveq2 
 |-  ( f = i -> ( D A f ) = ( D A i ) )
205 105 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> i e. M )
206 ovexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( D A i ) e. _V )
207 6 204 205 206 fvmptd3 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( F ` i ) = ( D A i ) )
208 4 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> A = ( d e. P , f e. M |-> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) ) )
209 simpr 
 |-  ( ( d = D /\ f = i ) -> f = i )
210 coeq2 
 |-  ( d = D -> ( x o. d ) = ( x o. D ) )
211 210 adantr 
 |-  ( ( d = D /\ f = i ) -> ( x o. d ) = ( x o. D ) )
212 209 211 fveq12d 
 |-  ( ( d = D /\ f = i ) -> ( f ` ( x o. d ) ) = ( i ` ( x o. D ) ) )
213 212 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 ) ) ) )
214 coeq1 
 |-  ( x = t -> ( x o. D ) = ( t o. D ) )
215 214 fveq2d 
 |-  ( x = t -> ( i ` ( x o. D ) ) = ( i ` ( t o. D ) ) )
216 215 cbvmptv 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( x o. D ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) )
217 213 216 eqtrdi 
 |-  ( ( d = D /\ f = i ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) ) )
218 217 adantl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ ( d = D /\ f = i ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) ) )
219 147 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> D e. P )
220 79 a1i 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
221 220 mptexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) ) e. _V )
222 208 218 219 205 221 ovmpod 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( D A i ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) ) )
223 207 222 eqtrd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( F ` i ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( i ` ( t o. D ) ) ) )
224 fvexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( i ` ( y o. D ) ) e. _V )
225 203 223 151 224 fvmptd4 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( ( F ` i ) ` y ) = ( i ` ( y o. D ) ) )
226 225 adantlr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( ( F ` i ) ` y ) = ( i ` ( y o. D ) ) )
227 oveq2 
 |-  ( f = j -> ( D A f ) = ( D A j ) )
228 simpr 
 |-  ( ( d = D /\ f = j ) -> f = j )
229 210 adantr 
 |-  ( ( d = D /\ f = j ) -> ( x o. d ) = ( x o. D ) )
230 228 229 fveq12d 
 |-  ( ( d = D /\ f = j ) -> ( f ` ( x o. d ) ) = ( j ` ( x o. D ) ) )
231 230 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 ) ) ) )
232 214 fveq2d 
 |-  ( x = t -> ( j ` ( x o. D ) ) = ( j ` ( t o. D ) ) )
233 232 cbvmptv 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( x o. D ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) )
234 231 233 eqtrdi 
 |-  ( ( d = D /\ f = j ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
235 234 adantl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ ( d = D /\ f = j ) ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( f ` ( x o. d ) ) ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
236 simplr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> j e. M )
237 220 mptexd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) e. _V )
238 208 235 219 236 237 ovmpod 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( D A j ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
239 227 238 sylan9eqr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ f = j ) -> ( D A f ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
240 239 adantllr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ f = j ) -> ( D A f ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
241 125 ad2antrr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> j e. M )
242 79 a1i 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
243 242 mptexd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) e. _V )
244 6 240 241 243 fvmptd2 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( F ` j ) = ( t e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( j ` ( t o. D ) ) ) )
245 coeq1 
 |-  ( t = ( x oF - y ) -> ( t o. D ) = ( ( x oF - y ) o. D ) )
246 245 fveq2d 
 |-  ( t = ( x oF - y ) -> ( j ` ( t o. D ) ) = ( j ` ( ( x oF - y ) o. D ) ) )
247 246 adantl 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> ( j ` ( t o. D ) ) = ( j ` ( ( x oF - y ) o. D ) ) )
248 160 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> x : I --> NN0 )
249 248 ffnd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> x Fn I )
250 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> I e. V )
251 49 a1i 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> NN0 e. _V )
252 157 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> y e. ( NN0 ^m I ) )
253 250 251 252 elmaprd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> y : I --> NN0 )
254 253 ffnd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> y Fn I )
255 62 ad5antr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> D : I --> I )
256 inidm 
 |-  ( I i^i I ) = I
257 249 254 255 250 250 250 256 ofco 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> ( ( x oF - y ) o. D ) = ( ( x o. D ) oF - ( y o. D ) ) )
258 257 fveq2d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> ( j ` ( ( x oF - y ) o. D ) ) = ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) )
259 247 258 eqtrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ t = ( x oF - y ) ) -> ( j ` ( t o. D ) ) = ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) )
260 breq1 
 |-  ( h = ( x oF - y ) -> ( h finSupp 0 <-> ( x oF - y ) finSupp 0 ) )
261 162 159 146 146 256 offn 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) Fn I )
262 162 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> x Fn I )
263 159 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> y Fn I )
264 146 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> I e. V )
265 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> a e. I )
266 fnfvof 
 |-  ( ( ( x Fn I /\ y Fn I ) /\ ( I e. V /\ a e. I ) ) -> ( ( x oF - y ) ` a ) = ( ( x ` a ) - ( y ` a ) ) )
267 262 263 264 265 266 syl22anc 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( ( x oF - y ) ` a ) = ( ( x ` a ) - ( y ` a ) ) )
268 158 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( y ` a ) e. NN0 )
269 161 ffvelcdmda 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( x ` a ) e. NN0 )
270 simplr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } )
271 164 270 elrabrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> y oR <_ x )
272 263 262 264 271 265 fnfvor 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( y ` a ) <_ ( x ` a ) )
273 nn0sub 
 |-  ( ( ( y ` a ) e. NN0 /\ ( x ` a ) e. NN0 ) -> ( ( y ` a ) <_ ( x ` a ) <-> ( ( x ` a ) - ( y ` a ) ) e. NN0 ) )
274 273 biimpa 
 |-  ( ( ( ( y ` a ) e. NN0 /\ ( x ` a ) e. NN0 ) /\ ( y ` a ) <_ ( x ` a ) ) -> ( ( x ` a ) - ( y ` a ) ) e. NN0 )
275 268 269 272 274 syl21anc 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( ( x ` a ) - ( y ` a ) ) e. NN0 )
276 267 275 eqeltrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. I ) -> ( ( x oF - y ) ` a ) e. NN0 )
277 276 ralrimiva 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> A. a e. I ( ( x oF - y ) ` a ) e. NN0 )
278 ffnfv 
 |-  ( ( x oF - y ) : I --> NN0 <-> ( ( x oF - y ) Fn I /\ A. a e. I ( ( x oF - y ) ` a ) e. NN0 ) )
279 261 277 278 sylanbrc 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) : I --> NN0 )
280 154 146 279 elmapdd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) e. ( NN0 ^m I ) )
281 ovexd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) e. _V )
282 43 a1i 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> 0 e. NN0 )
283 162 159 146 146 offun 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> Fun ( x oF - y ) )
284 23 psrbagfsupp 
 |-  ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> x finSupp 0 )
285 284 ad2antlr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> x finSupp 0 )
286 dffn2 
 |-  ( ( x oF - y ) Fn I <-> ( x oF - y ) : I --> _V )
287 261 286 sylib 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) : I --> _V )
288 162 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> x Fn I )
289 159 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> y Fn I )
290 146 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> I e. V )
291 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> a e. ( I \ ( x supp 0 ) ) )
292 291 eldifad 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> a e. I )
293 288 289 290 292 266 syl22anc 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( ( x oF - y ) ` a ) = ( ( x ` a ) - ( y ` a ) ) )
294 43 a1i 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> 0 e. NN0 )
295 288 290 294 291 fvdifsupp 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( x ` a ) = 0 )
296 158 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> y : I --> NN0 )
297 296 292 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( y ` a ) e. NN0 )
298 simplr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } )
299 164 298 elrabrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> y oR <_ x )
300 289 288 290 299 292 fnfvor 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( y ` a ) <_ ( x ` a ) )
301 300 295 breqtrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( y ` a ) <_ 0 )
302 nn0le0eq0 
 |-  ( ( y ` a ) e. NN0 -> ( ( y ` a ) <_ 0 <-> ( y ` a ) = 0 ) )
303 302 biimpa 
 |-  ( ( ( y ` a ) e. NN0 /\ ( y ` a ) <_ 0 ) -> ( y ` a ) = 0 )
304 297 301 303 syl2anc 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( y ` a ) = 0 )
305 295 304 oveq12d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( ( x ` a ) - ( y ` a ) ) = ( 0 - 0 ) )
306 0m0e0 
 |-  ( 0 - 0 ) = 0
307 306 a1i 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( 0 - 0 ) = 0 )
308 293 305 307 3eqtrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) /\ a e. ( I \ ( x supp 0 ) ) ) -> ( ( x oF - y ) ` a ) = 0 )
309 287 308 suppss 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( ( x oF - y ) supp 0 ) C_ ( x supp 0 ) )
310 281 282 283 285 309 fsuppsssuppgd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) finSupp 0 )
311 260 280 310 elrabd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( x oF - y ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
312 fvexd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) e. _V )
313 244 259 311 312 fvmptd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( ( F ` j ) ` ( x oF - y ) ) = ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) )
314 226 313 oveq12d 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } ) -> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) = ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) ) )
315 314 mpteq2dva 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) ) = ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) ) ) )
316 315 oveq2d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) ) ) = ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( i ` ( y o. D ) ) ( .r ` R ) ( j ` ( ( x o. D ) oF - ( y o. D ) ) ) ) ) ) )
317 201 316 eqtr4d 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) = ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) ) ) )
318 317 mpteq2dva 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) ) ) ) )
319 oveq2 
 |-  ( f = ( i ( .r ` W ) j ) -> ( D A f ) = ( D A ( i ( .r ` W ) j ) ) )
320 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 ) ) ) ) )
321 simprr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) -> f = ( i ( .r ` W ) j ) )
322 7 11 117 13 23 105 125 mplmul 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( i ( .r ` W ) j ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) ) ) )
323 322 adantr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) -> ( i ( .r ` W ) j ) = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) ) ) )
324 321 323 eqtrd 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) -> f = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) ) ) )
325 324 adantr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> f = ( u e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) ) ) )
326 simpr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> u = ( x o. d ) )
327 simplrl 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> d = D )
328 327 adantr 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> d = D )
329 328 coeq2d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( x o. d ) = ( x o. D ) )
330 326 329 eqtrd 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> u = ( x o. D ) )
331 330 breq2d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( w oR <_ u <-> w oR <_ ( x o. D ) ) )
332 331 rabbidv 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } = { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } )
333 330 fvoveq1d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( j ` ( u oF - v ) ) = ( j ` ( ( x o. D ) oF - v ) ) )
334 333 oveq2d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) = ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) )
335 332 334 mpteq12dv 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) = ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) )
336 335 oveq2d 
 |-  ( ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) /\ u = ( x o. d ) ) -> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ u } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( u oF - v ) ) ) ) ) = ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) )
337 5 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> I e. V )
338 9 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> D e. P )
339 327 338 eqeltrd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> d e. P )
340 simpr 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> x e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
341 1 2 337 339 340 mplvrpmlem 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( x o. d ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } )
342 ovexd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) e. _V )
343 325 336 341 342 fvmptd 
 |-  ( ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` W ) j ) ) ) /\ x e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) -> ( f ` ( x o. d ) ) = ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) )
344 343 mpteq2dva 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ ( d = D /\ f = ( i ( .r ` 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 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) )
345 14 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> W e. Ring )
346 11 13 345 105 125 ringcld 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( i ( .r ` W ) j ) e. M )
347 79 a1i 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> { h e. ( NN0 ^m I ) | h finSupp 0 } e. _V )
348 347 mptexd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) e. _V )
349 320 344 147 346 348 ovmpod 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( D A ( i ( .r ` W ) j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) )
350 319 349 sylan9eqr 
 |-  ( ( ( ( ph /\ i e. M ) /\ j e. M ) /\ f = ( i ( .r ` W ) j ) ) -> ( D A f ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) )
351 6 350 346 348 fvmptd2 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( .r ` W ) j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( v e. { w e. { h e. ( NN0 ^m I ) | h finSupp 0 } | w oR <_ ( x o. D ) } |-> ( ( i ` v ) ( .r ` R ) ( j ` ( ( x o. D ) oF - v ) ) ) ) ) ) )
352 1 2 3 4 5 mplvrpmga 
 |-  ( ph -> A e. ( S GrpAct M ) )
353 2 gaf 
 |-  ( A e. ( S GrpAct M ) -> A : ( P X. M ) --> M )
354 352 353 syl 
 |-  ( ph -> A : ( P X. M ) --> M )
355 354 fovcld 
 |-  ( ( ph /\ D e. P /\ f e. M ) -> ( D A f ) e. M )
356 355 3expa 
 |-  ( ( ( ph /\ D e. P ) /\ f e. M ) -> ( D A f ) e. M )
357 356 an32s 
 |-  ( ( ( ph /\ f e. M ) /\ D e. P ) -> ( D A f ) e. M )
358 9 357 mpidan 
 |-  ( ( ph /\ f e. M ) -> ( D A f ) e. M )
359 358 6 fmptd 
 |-  ( ph -> F : M --> M )
360 359 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> F : M --> M )
361 360 105 ffvelcdmd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` i ) e. M )
362 360 125 ffvelcdmd 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` j ) e. M )
363 7 11 117 13 23 361 362 mplmul 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( ( F ` i ) ( .r ` W ) ( F ` j ) ) = ( x e. { h e. ( NN0 ^m I ) | h finSupp 0 } |-> ( R gsum ( y e. { z e. { h e. ( NN0 ^m I ) | h finSupp 0 } | z oR <_ x } |-> ( ( ( F ` i ) ` y ) ( .r ` R ) ( ( F ` j ) ` ( x oF - y ) ) ) ) ) ) )
364 318 351 363 3eqtr4d 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( .r ` W ) j ) ) = ( ( F ` i ) ( .r ` W ) ( F ` j ) ) )
365 364 anasss 
 |-  ( ( ph /\ ( i e. M /\ j e. M ) ) -> ( F ` ( i ( .r ` W ) j ) ) = ( ( F ` i ) ( .r ` W ) ( F ` j ) ) )
366 eqid 
 |-  ( +g ` W ) = ( +g ` W )
367 1 2 3 4 5 6 7 8 9 mplvrpmmhm 
 |-  ( ph -> F e. ( W MndHom W ) )
368 367 ad2antrr 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> F e. ( W MndHom W ) )
369 11 366 366 mhmlin 
 |-  ( ( F e. ( W MndHom W ) /\ i e. M /\ j e. M ) -> ( F ` ( i ( +g ` W ) j ) ) = ( ( F ` i ) ( +g ` W ) ( F ` j ) ) )
370 368 105 125 369 syl3anc 
 |-  ( ( ( ph /\ i e. M ) /\ j e. M ) -> ( F ` ( i ( +g ` W ) j ) ) = ( ( F ` i ) ( +g ` W ) ( F ` j ) ) )
371 370 anasss 
 |-  ( ( ph /\ ( i e. M /\ j e. M ) ) -> ( F ` ( i ( +g ` W ) j ) ) = ( ( F ` i ) ( +g ` W ) ( F ` j ) ) )
372 11 12 12 13 13 14 14 92 365 11 366 366 359 371 isrhmd 
 |-  ( ph -> F e. ( W RingHom W ) )