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