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 ) )

Metamath Proof Explorer

Theorem mplvrpmrhm

Proof