Theorem evlselv

Description: Evaluating a selection of variable assignments, then evaluating the rest of the variables, is the same as evaluating with all assignments. (Contributed by SN, 10-Mar-2025)

	Ref	Expression
Hypotheses	evlselv.p	|- P = ( I mPoly R )
	evlselv.k	|- K = ( Base ` R )
	evlselv.b	|- B = ( Base ` P )
	evlselv.u	|- U = ( ( I \ J ) mPoly R )
	evlselv.t	|- T = ( J mPoly U )
	evlselv.l	|- L = ( algSc ` U )
	evlselv.i	|- ( ph -> I e. V )
	evlselv.r	|- ( ph -> R e. CRing )
	evlselv.j	|- ( ph -> J C_ I )
	evlselv.f	|- ( ph -> F e. B )
	evlselv.a	|- ( ph -> A e. ( K ^m I ) )
Assertion	evlselv	|- ( ph -> ( ( ( ( I \ J ) eval R ) ` ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ) ` ( A |` ( I \ J ) ) ) = ( ( ( I eval R ) ` F ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		evlselv.p	|- P = ( I mPoly R )
2		evlselv.k	|- K = ( Base ` R )
3		evlselv.b	|- B = ( Base ` P )
4		evlselv.u	|- U = ( ( I \ J ) mPoly R )
5		evlselv.t	|- T = ( J mPoly U )
6		evlselv.l	|- L = ( algSc ` U )
7		evlselv.i	|- ( ph -> I e. V )
8		evlselv.r	|- ( ph -> R e. CRing )
9		evlselv.j	|- ( ph -> J C_ I )
10		evlselv.f	|- ( ph -> F e. B )
11		evlselv.a	|- ( ph -> A e. ( K ^m I ) )
12		eqid	|- ( Base ` U ) = ( Base ` U )
13		eqid	|- ( .r ` U ) = ( .r ` U )
14		difssd	|- ( ph -> ( I \ J ) C_ I )
15	7 14	ssexd	|- ( ph -> ( I \ J ) e. _V )
16	4 15 8	mplcrngd	|- ( ph -> U e. CRing )
17	16	crngringd	|- ( ph -> U e. Ring )
18	17	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> U e. Ring )
19		eqid	|- ( Base ` T ) = ( Base ` T )
20		eqid	|- { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } = { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin }
21	1 3 4 5 19 8 9 10	selvcl	|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) e. ( Base ` T ) )
22	5 12 19 20 21	mplelf	|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) : { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } --> ( Base ` U ) )
23	22	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( I selectVars R ) ` J ) ` F ) : { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } --> ( Base ` U ) )
24	23	ffvelcdmda	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) e. ( Base ` U ) )
25		eqid	|- ( mulGrp ` U ) = ( mulGrp ` U )
26		eqid	|- ( .g ` ( mulGrp ` U ) ) = ( .g ` ( mulGrp ` U ) )
27	7 9	ssexd	|- ( ph -> J e. _V )
28	27	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> J e. _V )
29	16	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> U e. CRing )
30		fvexd	|- ( ph -> ( Base ` U ) e. _V )
31	2	fvexi	|- K e. _V
32	31	a1i	|- ( ph -> K e. _V )
33	8	crngringd	|- ( ph -> R e. Ring )
34	4 12 2 6 15 33	mplasclf	|- ( ph -> L : K --> ( Base ` U ) )
35	30 32 34	elmapdd	|- ( ph -> L e. ( ( Base ` U ) ^m K ) )
36	11 9	elmapssresd	|- ( ph -> ( A |` J ) e. ( K ^m J ) )
37	35 36	mapcod	|- ( ph -> ( L o. ( A |` J ) ) e. ( ( Base ` U ) ^m J ) )
38	37	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( L o. ( A |` J ) ) e. ( ( Base ` U ) ^m J ) )
39		simpr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } )
40	20 12 25 26 28 29 38 39	evlsvvvallem	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) e. ( Base ` U ) )
41	12 13 18 24 40	ringcld	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) e. ( Base ` U ) )
42		eqidd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) )
43		eqidd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( u e. ( Base ` U ) |-> ( u ` c ) ) = ( u e. ( Base ` U ) |-> ( u ` c ) ) )
44		fveq1	|- ( u = ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) -> ( u ` c ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ` c ) )
45	41 42 43 44	fmptco	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ` c ) ) )
46	34	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> L : K --> ( Base ` U ) )
47		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
48	47 2	mgpbas	|- K = ( Base ` ( mulGrp ` R ) )
49		eqid	|- ( .g ` ( mulGrp ` R ) ) = ( .g ` ( mulGrp ` R ) )
50	47	ringmgp	|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
51	33 50	syl	|- ( ph -> ( mulGrp ` R ) e. Mnd )
52	51	ad3antrrr	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( mulGrp ` R ) e. Mnd )
53	20	psrbagf	|- ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } -> e : J --> NN0 )
54	53	adantl	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> e : J --> NN0 )
55	54	ffvelcdmda	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( e ` j ) e. NN0 )
56		elmapi	|- ( A e. ( K ^m I ) -> A : I --> K )
57	11 56	syl	|- ( ph -> A : I --> K )
58	57 9	fssresd	|- ( ph -> ( A |` J ) : J --> K )
59	58	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( A |` J ) : J --> K )
60	59	ffvelcdmda	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( A |` J ) ` j ) e. K )
61	48 49 52 55 60	mulgnn0cld	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) e. K )
62	46 61	cofmpt	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( L o. ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( j e. J |-> ( L ` ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
63	4	mplassa	|- ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. AssAlg )
64	15 8 63	syl2anc	|- ( ph -> U e. AssAlg )
65		eqid	|- ( Scalar ` U ) = ( Scalar ` U )
66	6 65	asclrhm	|- ( U e. AssAlg -> L e. ( ( Scalar ` U ) RingHom U ) )
67	64 66	syl	|- ( ph -> L e. ( ( Scalar ` U ) RingHom U ) )
68	4 15 8	mplsca	|- ( ph -> R = ( Scalar ` U ) )
69	68	eqcomd	|- ( ph -> ( Scalar ` U ) = R )
70	69	oveq1d	|- ( ph -> ( ( Scalar ` U ) RingHom U ) = ( R RingHom U ) )
71	67 70	eleqtrd	|- ( ph -> L e. ( R RingHom U ) )
72	47 25	rhmmhm	|- ( L e. ( R RingHom U ) -> L e. ( ( mulGrp ` R ) MndHom ( mulGrp ` U ) ) )
73	71 72	syl	|- ( ph -> L e. ( ( mulGrp ` R ) MndHom ( mulGrp ` U ) ) )
74	73	ad3antrrr	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> L e. ( ( mulGrp ` R ) MndHom ( mulGrp ` U ) ) )
75	48 49 26	mhmmulg	|- ( ( L e. ( ( mulGrp ` R ) MndHom ( mulGrp ` U ) ) /\ ( e ` j ) e. NN0 /\ ( ( A |` J ) ` j ) e. K ) -> ( L ` ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( L ` ( ( A |` J ) ` j ) ) ) )
76	74 55 60 75	syl3anc	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( L ` ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( L ` ( ( A |` J ) ` j ) ) ) )
77	58	ad3antrrr	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( A |` J ) : J --> K )
78		simpr	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> j e. J )
79	77 78	fvco3d	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( L o. ( A |` J ) ) ` j ) = ( L ` ( ( A |` J ) ` j ) ) )
80	79	oveq2d	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) = ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( L ` ( ( A |` J ) ` j ) ) ) )
81	76 80	eqtr4d	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( L ` ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) )
82	81	mpteq2dva	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( L ` ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) )
83	62 82	eqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( L o. ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) )
84	83	oveq2d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` U ) gsum ( L o. ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) = ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) )
85		eqid	|- ( Base ` ( mulGrp ` ( Scalar ` U ) ) ) = ( Base ` ( mulGrp ` ( Scalar ` U ) ) )
86		eqid	|- ( 0g ` ( mulGrp ` ( Scalar ` U ) ) ) = ( 0g ` ( mulGrp ` ( Scalar ` U ) ) )
87	68 8	eqeltrrd	|- ( ph -> ( Scalar ` U ) e. CRing )
88		eqid	|- ( mulGrp ` ( Scalar ` U ) ) = ( mulGrp ` ( Scalar ` U ) )
89	88	crngmgp	|- ( ( Scalar ` U ) e. CRing -> ( mulGrp ` ( Scalar ` U ) ) e. CMnd )
90	87 89	syl	|- ( ph -> ( mulGrp ` ( Scalar ` U ) ) e. CMnd )
91	90	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( mulGrp ` ( Scalar ` U ) ) e. CMnd )
92	25	ringmgp	|- ( U e. Ring -> ( mulGrp ` U ) e. Mnd )
93	17 92	syl	|- ( ph -> ( mulGrp ` U ) e. Mnd )
94	93	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( mulGrp ` U ) e. Mnd )
95	88 25	rhmmhm	|- ( L e. ( ( Scalar ` U ) RingHom U ) -> L e. ( ( mulGrp ` ( Scalar ` U ) ) MndHom ( mulGrp ` U ) ) )
96	67 95	syl	|- ( ph -> L e. ( ( mulGrp ` ( Scalar ` U ) ) MndHom ( mulGrp ` U ) ) )
97	96	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> L e. ( ( mulGrp ` ( Scalar ` U ) ) MndHom ( mulGrp ` U ) ) )
98	68	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` U ) ) )
99	2 98	eqtrid	|- ( ph -> K = ( Base ` ( Scalar ` U ) ) )
100	99	ad3antrrr	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> K = ( Base ` ( Scalar ` U ) ) )
101	61 100	eleqtrd	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) e. ( Base ` ( Scalar ` U ) ) )
102		eqid	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
103	88 102	mgpbas	|- ( Base ` ( Scalar ` U ) ) = ( Base ` ( mulGrp ` ( Scalar ` U ) ) )
104	101 103	eleqtrdi	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ j e. J ) -> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) e. ( Base ` ( mulGrp ` ( Scalar ` U ) ) ) )
105	104	fmpttd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) : J --> ( Base ` ( mulGrp ` ( Scalar ` U ) ) ) )
106	54	feqmptd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> e = ( j e. J |-> ( e ` j ) ) )
107	20	psrbagfsupp	|- ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } -> e finSupp 0 )
108	107	adantl	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> e finSupp 0 )
109	106 108	eqbrtrrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( e ` j ) ) finSupp 0 )
110		eqid	|- ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
111	48 110 49	mulg0	|- ( k e. K -> ( 0 ( .g ` ( mulGrp ` R ) ) k ) = ( 0g ` ( mulGrp ` R ) ) )
112	111	adantl	|- ( ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ k e. K ) -> ( 0 ( .g ` ( mulGrp ` R ) ) k ) = ( 0g ` ( mulGrp ` R ) ) )
113		fvexd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( 0g ` ( mulGrp ` R ) ) e. _V )
114	109 112 55 60 113	fsuppssov1	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) finSupp ( 0g ` ( mulGrp ` R ) ) )
115		eqid	|- ( 1r ` R ) = ( 1r ` R )
116	47 115	ringidval	|- ( 1r ` R ) = ( 0g ` ( mulGrp ` R ) )
117	114 116	breqtrrdi	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) finSupp ( 1r ` R ) )
118	68	fveq2d	|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` U ) ) )
119		eqid	|- ( 1r ` ( Scalar ` U ) ) = ( 1r ` ( Scalar ` U ) )
120	88 119	ringidval	|- ( 1r ` ( Scalar ` U ) ) = ( 0g ` ( mulGrp ` ( Scalar ` U ) ) )
121	118 120	eqtrdi	|- ( ph -> ( 1r ` R ) = ( 0g ` ( mulGrp ` ( Scalar ` U ) ) ) )
122	121	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( 1r ` R ) = ( 0g ` ( mulGrp ` ( Scalar ` U ) ) ) )
123	117 122	breqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) finSupp ( 0g ` ( mulGrp ` ( Scalar ` U ) ) ) )
124	85 86 91 94 28 97 105 123	gsummhm	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` U ) gsum ( L o. ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) = ( L ` ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
125	84 124	eqtr3d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) = ( L ` ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
126	125	oveq2d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) = ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( L ` ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) )
127	64	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> U e. AssAlg )
128	101	fmpttd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) : J --> ( Base ` ( Scalar ` U ) ) )
129	123 120	breqtrrdi	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) finSupp ( 1r ` ( Scalar ` U ) ) )
130	103 120 91 28 128 129	gsumcl	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. ( Base ` ( Scalar ` U ) ) )
131		eqid	|- ( .s ` U ) = ( .s ` U )
132	6 65 102 12 13 131	asclmul2	|- ( ( U e. AssAlg /\ ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. ( Base ` ( Scalar ` U ) ) /\ ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) e. ( Base ` U ) ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( L ` ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .s ` U ) ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ) )
133	127 130 24 132	syl3anc	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( L ` ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .s ` U ) ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ) )
134	126 133	eqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .s ` U ) ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ) )
135	134	fveq1d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ` c ) = ( ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .s ` U ) ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ) ` c ) )
136		eqid	|- ( .r ` R ) = ( .r ` R )
137		eqid	|- { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin }
138	99	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> K = ( Base ` ( Scalar ` U ) ) )
139	130 138	eleqtrrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. K )
140		simplr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } )
141	4 131 2 12 136 137 139 24 140	mplvscaval	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .s ` U ) ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ) ` c ) = ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) )
142	135 141	eqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ` c ) = ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) )
143	142	mpteq2dva	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ` c ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) ) )
144	45 143	eqtrd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) ) )
145	144	oveq2d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) ) ) )
146	69	fveq2d	|- ( ph -> ( mulGrp ` ( Scalar ` U ) ) = ( mulGrp ` R ) )
147	146	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( mulGrp ` ( Scalar ` U ) ) = ( mulGrp ` R ) )
148	147	oveq1d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
149	148	oveq1d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) = ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) )
150	8	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> R e. CRing )
151	148 139	eqeltrrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. K )
152	22	ffvelcdmda	|- ( ( ph /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) e. ( Base ` U ) )
153	4 2 12 137 152	mplelf	|- ( ( ph /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) : { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } --> K )
154	153	ffvelcdmda	|- ( ( ( ph /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) e. K )
155	154	an32s	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) e. K )
156	2 136 150 151 155	crngcomd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
157	149 156	eqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
158	157	mpteq2dva	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) )
159	158	oveq2d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( mulGrp ` ( Scalar ` U ) ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) ) )
160	145 159	eqtrd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) ) )
161	160	oveq1d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
162		eqid	|- ( u e. ( Base ` U ) |-> ( u ` c ) ) = ( u e. ( Base ` U ) |-> ( u ` c ) )
163		fveq1	|- ( u = ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) -> ( u ` c ) = ( ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ` c ) )
164		eqid	|- ( J eval U ) = ( J eval U )
165	164 5 19 20 12 25 26 13 27 16 21 37	evlvvval	|- ( ph -> ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) = ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) )
166	164 5 19 12 27 16 21 37	evlcl	|- ( ph -> ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) e. ( Base ` U ) )
167	165 166	eqeltrrd	|- ( ph -> ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) e. ( Base ` U ) )
168	167	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) e. ( Base ` U ) )
169		fvexd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ` c ) e. _V )
170	162 163 168 169	fvmptd3	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( u e. ( Base ` U ) |-> ( u ` c ) ) ` ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) = ( ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ` c ) )
171		eqid	|- ( 0g ` U ) = ( 0g ` U )
172	17	ringcmnd	|- ( ph -> U e. CMnd )
173	172	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> U e. CMnd )
174	8	crnggrpd	|- ( ph -> R e. Grp )
175	174	grpmndd	|- ( ph -> R e. Mnd )
176	175	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> R e. Mnd )
177		ovex	|- ( NN0 ^m J ) e. _V
178	177	rabex	|- { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } e. _V
179	178	a1i	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } e. _V )
180	15	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( I \ J ) e. _V )
181	174	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> R e. Grp )
182		simpr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } )
183	4 12 137 162 180 181 182	mplmapghm	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( u e. ( Base ` U ) |-> ( u ` c ) ) e. ( U GrpHom R ) )
184		ghmmhm	|- ( ( u e. ( Base ` U ) |-> ( u ` c ) ) e. ( U GrpHom R ) -> ( u e. ( Base ` U ) |-> ( u ` c ) ) e. ( U MndHom R ) )
185	183 184	syl	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( u e. ( Base ` U ) |-> ( u ` c ) ) e. ( U MndHom R ) )
186	41	fmpttd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) : { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } --> ( Base ` U ) )
187	27	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> J e. _V )
188	16	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> U e. CRing )
189	21	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( I selectVars R ) ` J ) ` F ) e. ( Base ` T ) )
190	37	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( L o. ( A |` J ) ) e. ( ( Base ` U ) ^m J ) )
191	20 5 19 12 25 26 13 187 188 189 190	evlvvvallem	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) finSupp ( 0g ` U ) )
192	12 171 173 176 179 185 186 191	gsummhm	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) = ( ( u e. ( Base ` U ) |-> ( u ` c ) ) ` ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) )
193	165	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) = ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) )
194	193	fveq1d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) = ( ( U gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ` c ) )
195	170 192 194	3eqtr4rd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) = ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) )
196	195	oveq1d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( R gsum ( ( u e. ( Base ` U ) |-> ( u ` c ) ) o. ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ( .r ` U ) ( ( mulGrp ` U ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` U ) ) ( ( L o. ( A |` J ) ) ` j ) ) ) ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
197		eqid	|- ( 0g ` R ) = ( 0g ` R )
198	33	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> R e. Ring )
199	47	crngmgp	|- ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
200	8 199	syl	|- ( ph -> ( mulGrp ` R ) e. CMnd )
201	200	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( mulGrp ` R ) e. CMnd )
202	51	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( mulGrp ` R ) e. Mnd )
203	137	psrbagf	|- ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> c : ( I \ J ) --> NN0 )
204	203	adantl	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> c : ( I \ J ) --> NN0 )
205	204	ffvelcdmda	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( c ` k ) e. NN0 )
206	57 14	fssresd	|- ( ph -> ( A |` ( I \ J ) ) : ( I \ J ) --> K )
207	206	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( A |` ( I \ J ) ) : ( I \ J ) --> K )
208	207	ffvelcdmda	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( A |` ( I \ J ) ) ` k ) e. K )
209	48 49 202 205 208	mulgnn0cld	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) e. K )
210	209	fmpttd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) : ( I \ J ) --> K )
211	204	feqmptd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> c = ( k e. ( I \ J ) |-> ( c ` k ) ) )
212	137	psrbagfsupp	|- ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> c finSupp 0 )
213	212	adantl	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> c finSupp 0 )
214	211 213	eqbrtrrd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( c ` k ) ) finSupp 0 )
215	48 110 49	mulg0	|- ( v e. K -> ( 0 ( .g ` ( mulGrp ` R ) ) v ) = ( 0g ` ( mulGrp ` R ) ) )
216	215	adantl	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ v e. K ) -> ( 0 ( .g ` ( mulGrp ` R ) ) v ) = ( 0g ` ( mulGrp ` R ) ) )
217		fvexd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( c ` k ) e. _V )
218		fvexd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( 0g ` ( mulGrp ` R ) ) e. _V )
219	214 216 217 208 218	fsuppssov1	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` R ) ) )
220	48 110 201 180 210 219	gsumcl	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) e. K )
221	33	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> R e. Ring )
222	2 136 221 155 151	ringcld	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) e. K )
223	178	mptex	|- ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) e. _V
224	223	a1i	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) e. _V )
225		fvexd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( 0g ` R ) e. _V )
226		funmpt	|- Fun ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) )
227	226	a1i	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> Fun ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) )
228	5 19 171 21 16	mplelsfi	|- ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) finSupp ( 0g ` U ) )
229	228	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( I selectVars R ) ` J ) ` F ) finSupp ( 0g ` U ) )
230		ssidd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) C_ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) )
231		fvexd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( 0g ` U ) e. _V )
232	23 230 179 231	suppssr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. ( { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } \ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) ) ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) = ( 0g ` U ) )
233	232	fveq1d	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. ( { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } \ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) ) ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) = ( ( 0g ` U ) ` c ) )
234	4 137 197 171 15 174	mpl0	|- ( ph -> ( 0g ` U ) = ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) )
235	234	adantr	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( 0g ` U ) = ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) )
236	235	fveq1d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( 0g ` U ) ` c ) = ( ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) ` c ) )
237		fvex	|- ( 0g ` R ) e. _V
238	237	fvconst2	|- ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> ( ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) ` c ) = ( 0g ` R ) )
239	238	adantl	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { ( 0g ` R ) } ) ` c ) = ( 0g ` R ) )
240	236 239	eqtrd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( 0g ` U ) ` c ) = ( 0g ` R ) )
241	240	adantr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. ( { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } \ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) ) ) -> ( ( 0g ` U ) ` c ) = ( 0g ` R ) )
242	233 241	eqtrd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. ( { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } \ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) ) ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) = ( 0g ` R ) )
243	242 179	suppss2	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) supp ( 0g ` R ) ) C_ ( ( ( ( I selectVars R ) ` J ) ` F ) supp ( 0g ` U ) ) )
244	224 225 227 229 243	fsuppsssuppgd	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ) finSupp ( 0g ` R ) )
245	33	ad2antrr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ v e. K ) -> R e. Ring )
246		simpr	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ v e. K ) -> v e. K )
247	2 136 197 245 246	ringlzd	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ v e. K ) -> ( ( 0g ` R ) ( .r ` R ) v ) = ( 0g ` R ) )
248	244 247 155 151 225	fsuppssov1	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) finSupp ( 0g ` R ) )
249	2 197 136 198 179 220 222 248	gsummulc1	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
250	161 196 249	3eqtr4d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) )
251		fveq2	|- ( a = e -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) = ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) )
252	251	adantl	|- ( ( b = c /\ a = e ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) = ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) )
253		simpl	|- ( ( b = c /\ a = e ) -> b = c )
254	252 253	fveq12d	|- ( ( b = c /\ a = e ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) = ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) )
255		fveq1	|- ( a = e -> ( a ` j ) = ( e ` j ) )
256	255	adantl	|- ( ( b = c /\ a = e ) -> ( a ` j ) = ( e ` j ) )
257	256	oveq1d	|- ( ( b = c /\ a = e ) -> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
258	257	mpteq2dv	|- ( ( b = c /\ a = e ) -> ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
259	258	oveq2d	|- ( ( b = c /\ a = e ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
260	254 259	oveq12d	|- ( ( b = c /\ a = e ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
261		fveq1	|- ( b = c -> ( b ` k ) = ( c ` k ) )
262	261	adantr	|- ( ( b = c /\ a = e ) -> ( b ` k ) = ( c ` k ) )
263	262	oveq1d	|- ( ( b = c /\ a = e ) -> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
264	263	mpteq2dv	|- ( ( b = c /\ a = e ) -> ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
265	264	oveq2d	|- ( ( b = c /\ a = e ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) = ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) )
266	260 265	oveq12d	|- ( ( b = c /\ a = e ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
267		eqid	|- ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) = ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
268		ovex	|- ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) e. _V
269	266 267 268	ovmpoa	|- ( ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
270	269	adantll	|- ( ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
271	270	mpteq2dva	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) = ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) )
272	271	oveq2d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` e ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( e ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) )
273	250 272	eqtr4d	|- ( ( ph /\ c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) )
274	273	mpteq2dva	|- ( ph -> ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) = ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) ) )
275	274	oveq2d	|- ( ph -> ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) ) ) )
276	33	ringcmnd	|- ( ph -> R e. CMnd )
277		ovex	|- ( NN0 ^m I ) e. _V
278	277	rabex	|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V
279	278	a1i	|- ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
280	33	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
281	22	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( I selectVars R ) ` J ) ` F ) : { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } --> ( Base ` U ) )
282		eqid	|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
283	7	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. V )
284	9	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> J C_ I )
285		simpr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
286	282 20 283 284 285	psrbagres	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` J ) e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } )
287	281 286	ffvelcdmd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) e. ( Base ` U ) )
288	4 2 12 137 287	mplelf	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) : { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } --> K )
289		difssd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( I \ J ) C_ I )
290	282 137 283 289 285	psrbagres	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` ( I \ J ) ) e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } )
291	288 290	ffvelcdmd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) e. K )
292	200	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( mulGrp ` R ) e. CMnd )
293	27	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> J e. _V )
294	51	ad2antrr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( mulGrp ` R ) e. Mnd )
295	282	psrbagf	|- ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d : I --> NN0 )
296	295	adantl	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d : I --> NN0 )
297	296 284	fssresd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` J ) : J --> NN0 )
298	297	ffvelcdmda	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( d |` J ) ` j ) e. NN0 )
299	58	ffvelcdmda	|- ( ( ph /\ j e. J ) -> ( ( A |` J ) ` j ) e. K )
300	299	adantlr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( A |` J ) ` j ) e. K )
301	48 49 294 298 300	mulgnn0cld	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) e. K )
302	301	fmpttd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) : J --> K )
303	27	mptexd	|- ( ph -> ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) e. _V )
304	303	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) e. _V )
305		fvexd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( 0g ` ( mulGrp ` R ) ) e. _V )
306		funmpt	|- Fun ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
307	306	a1i	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> Fun ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
308	282	psrbagfsupp	|- ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> d finSupp 0 )
309	308	adantl	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d finSupp 0 )
310		0zd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> 0 e. ZZ )
311	309 310	fsuppres	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` J ) finSupp 0 )
312		ssidd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d |` J ) supp 0 ) C_ ( ( d |` J ) supp 0 ) )
313	297 312 293 310	suppssr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. ( J \ ( ( d |` J ) supp 0 ) ) ) -> ( ( d |` J ) ` j ) = 0 )
314	313	oveq1d	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. ( J \ ( ( d |` J ) supp 0 ) ) ) -> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
315		eldifi	|- ( j e. ( J \ ( ( d |` J ) supp 0 ) ) -> j e. J )
316	48 110 49	mulg0	|- ( ( ( A |` J ) ` j ) e. K -> ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( 0g ` ( mulGrp ` R ) ) )
317	300 316	syl	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( 0g ` ( mulGrp ` R ) ) )
318	315 317	sylan2	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. ( J \ ( ( d |` J ) supp 0 ) ) ) -> ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( 0g ` ( mulGrp ` R ) ) )
319	314 318	eqtrd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. ( J \ ( ( d |` J ) supp 0 ) ) ) -> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( 0g ` ( mulGrp ` R ) ) )
320	319 293	suppss2	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) supp ( 0g ` ( mulGrp ` R ) ) ) C_ ( ( d |` J ) supp 0 ) )
321	304 305 307 311 320	fsuppsssuppgd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) finSupp ( 0g ` ( mulGrp ` R ) ) )
322	48 110 292 293 302 321	gsumcl	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. K )
323	2 136 280 291 322	ringcld	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) e. K )
324	15	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( I \ J ) e. _V )
325	51	ad2antrr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( mulGrp ` R ) e. Mnd )
326	296 289	fssresd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` ( I \ J ) ) : ( I \ J ) --> NN0 )
327	326	ffvelcdmda	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( d |` ( I \ J ) ) ` k ) e. NN0 )
328	206	ffvelcdmda	|- ( ( ph /\ k e. ( I \ J ) ) -> ( ( A |` ( I \ J ) ) ` k ) e. K )
329	328	adantlr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( A |` ( I \ J ) ) ` k ) e. K )
330	48 49 325 327 329	mulgnn0cld	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) e. K )
331	330	fmpttd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) : ( I \ J ) --> K )
332	324	mptexd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) e. _V )
333		funmpt	|- Fun ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
334	333	a1i	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> Fun ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
335	309 310	fsuppres	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d |` ( I \ J ) ) finSupp 0 )
336		ssidd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( d |` ( I \ J ) ) supp 0 ) C_ ( ( d |` ( I \ J ) ) supp 0 ) )
337	326 336 324 310	suppssr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) ) -> ( ( d |` ( I \ J ) ) ` k ) = 0 )
338	337	oveq1d	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) ) -> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
339		eldifi	|- ( k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) -> k e. ( I \ J ) )
340	339 329	sylan2	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) ) -> ( ( A |` ( I \ J ) ) ` k ) e. K )
341	48 110 49	mulg0	|- ( ( ( A |` ( I \ J ) ) ` k ) e. K -> ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( 0g ` ( mulGrp ` R ) ) )
342	340 341	syl	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) ) -> ( 0 ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( 0g ` ( mulGrp ` R ) ) )
343	338 342	eqtrd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( ( I \ J ) \ ( ( d |` ( I \ J ) ) supp 0 ) ) ) -> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( 0g ` ( mulGrp ` R ) ) )
344	343 324	suppss2	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) supp ( 0g ` ( mulGrp ` R ) ) ) C_ ( ( d |` ( I \ J ) ) supp 0 ) )
345	332 305 334 335 344	fsuppsssuppgd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` R ) ) )
346	48 110 292 324 331 345	gsumcl	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) e. K )
347	2 136 280 323 346	ringcld	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) e. K )
348	347	fmpttd	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> K )
349	8	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. CRing )
350	10	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> F e. B )
351	282 1 3 349 284 350 285	selvvvval	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) = ( F ` d ) )
352	351	mpteq2dva	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` d ) ) )
353		eqid	|- ( Base ` R ) = ( Base ` R )
354	1 353 3 282 10	mplelf	|- ( ph -> F : { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } --> ( Base ` R ) )
355	354	feqmptd	|- ( ph -> F = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` d ) ) )
356	1 3 197 10 8	mplelsfi	|- ( ph -> F finSupp ( 0g ` R ) )
357	355 356	eqbrtrrd	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( F ` d ) ) finSupp ( 0g ` R ) )
358	352 357	eqbrtrd	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ) finSupp ( 0g ` R ) )
359	33	adantr	|- ( ( ph /\ v e. K ) -> R e. Ring )
360		simpr	|- ( ( ph /\ v e. K ) -> v e. K )
361	2 136 197 359 360	ringlzd	|- ( ( ph /\ v e. K ) -> ( ( 0g ` R ) ( .r ` R ) v ) = ( 0g ` R ) )
362		fvexd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) e. _V )
363		fvexd	|- ( ph -> ( 0g ` R ) e. _V )
364	358 361 362 322 363	fsuppssov1	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ) finSupp ( 0g ` R ) )
365		ovexd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) e. _V )
366	364 361 365 346 363	fsuppssov1	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) finSupp ( 0g ` R ) )
367		eqid	|- ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) = ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) )
368	282 20 137 367 7 9	evlselvlem	|- ( ph -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -1-1-onto-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
369	2 197 276 279 348 366 368	gsumf1o	|- ( ph -> ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) o. ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) ) ) )
370	137	psrbagf	|- ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> b : ( I \ J ) --> NN0 )
371	370	ad2antrl	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> b : ( I \ J ) --> NN0 )
372	20	psrbagf	|- ( a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } -> a : J --> NN0 )
373	372	ad2antll	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> a : J --> NN0 )
374		disjdifr	|- ( ( I \ J ) i^i J ) = (/)
375	374	a1i	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( I \ J ) i^i J ) = (/) )
376	371 373 375	fun2d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( b u. a ) : ( ( I \ J ) u. J ) --> NN0 )
377		undifr	|- ( J C_ I <-> ( ( I \ J ) u. J ) = I )
378	9 377	sylib	|- ( ph -> ( ( I \ J ) u. J ) = I )
379	378	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( I \ J ) u. J ) = I )
380	379	feq2d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) : ( ( I \ J ) u. J ) --> NN0 <-> ( b u. a ) : I --> NN0 ) )
381	376 380	mpbid	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( b u. a ) : I --> NN0 )
382		vex	|- b e. _V
383		vex	|- a e. _V
384	382 383	unex	|- ( b u. a ) e. _V
385	384	a1i	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( b u. a ) e. _V )
386		0zd	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> 0 e. ZZ )
387	381	ffund	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> Fun ( b u. a ) )
388	137	psrbagfsupp	|- ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> b finSupp 0 )
389	388	ad2antrl	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> b finSupp 0 )
390	20	psrbagfsupp	|- ( a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } -> a finSupp 0 )
391	390	ad2antll	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> a finSupp 0 )
392	389 391	fsuppun	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) supp 0 ) e. Fin )
393	385 386 387 392	isfsuppd	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( b u. a ) finSupp 0 )
394		fcdmnn0fsuppg	|- ( ( ( b u. a ) e. _V /\ ( b u. a ) : I --> NN0 ) -> ( ( b u. a ) finSupp 0 <-> ( `' ( b u. a ) " NN ) e. Fin ) )
395	385 381 394	syl2anc	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) finSupp 0 <-> ( `' ( b u. a ) " NN ) e. Fin ) )
396	393 395	mpbid	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( `' ( b u. a ) " NN ) e. Fin )
397	7	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> I e. V )
398	282	psrbag	|- ( I e. V -> ( ( b u. a ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( ( b u. a ) : I --> NN0 /\ ( `' ( b u. a ) " NN ) e. Fin ) ) )
399	397 398	syl	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } <-> ( ( b u. a ) : I --> NN0 /\ ( `' ( b u. a ) " NN ) e. Fin ) ) )
400	381 396 399	mpbir2and	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( b u. a ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
401		eqidd	|- ( ph -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) = ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) )
402		eqidd	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) )
403		reseq1	|- ( d = ( b u. a ) -> ( d |` J ) = ( ( b u. a ) |` J ) )
404	403	fveq2d	|- ( d = ( b u. a ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) = ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) )
405		reseq1	|- ( d = ( b u. a ) -> ( d |` ( I \ J ) ) = ( ( b u. a ) |` ( I \ J ) ) )
406	404 405	fveq12d	|- ( d = ( b u. a ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) = ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) )
407	403	fveq1d	|- ( d = ( b u. a ) -> ( ( d |` J ) ` j ) = ( ( ( b u. a ) |` J ) ` j ) )
408	407	oveq1d	|- ( d = ( b u. a ) -> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
409	408	mpteq2dv	|- ( d = ( b u. a ) -> ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
410	409	oveq2d	|- ( d = ( b u. a ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
411	406 410	oveq12d	|- ( d = ( b u. a ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
412	405	fveq1d	|- ( d = ( b u. a ) -> ( ( d |` ( I \ J ) ) ` k ) = ( ( ( b u. a ) |` ( I \ J ) ) ` k ) )
413	412	oveq1d	|- ( d = ( b u. a ) -> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
414	413	mpteq2dv	|- ( d = ( b u. a ) -> ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
415	414	oveq2d	|- ( d = ( b u. a ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) = ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) )
416	411 415	oveq12d	|- ( d = ( b u. a ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
417	384 416	csbie	|- [_ ( b u. a ) / d ]_ ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) )
418	370	ffnd	|- ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } -> b Fn ( I \ J ) )
419	418	ad2antrl	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> b Fn ( I \ J ) )
420	373	ffnd	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> a Fn J )
421		fnunres2	|- ( ( b Fn ( I \ J ) /\ a Fn J /\ ( ( I \ J ) i^i J ) = (/) ) -> ( ( b u. a ) |` J ) = a )
422	419 420 375 421	syl3anc	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) |` J ) = a )
423	422	fveq2d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) = ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) )
424		fnunres1	|- ( ( b Fn ( I \ J ) /\ a Fn J /\ ( ( I \ J ) i^i J ) = (/) ) -> ( ( b u. a ) |` ( I \ J ) ) = b )
425	419 420 375 424	syl3anc	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( b u. a ) |` ( I \ J ) ) = b )
426	423 425	fveq12d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) = ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) )
427	422	fveq1d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( b u. a ) |` J ) ` j ) = ( a ` j ) )
428	427	oveq1d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
429	428	mpteq2dv	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) = ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
430	429	oveq2d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) = ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
431	426 430	oveq12d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) )
432	425	fveq1d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( b u. a ) |` ( I \ J ) ) ` k ) = ( b ` k ) )
433	432	oveq1d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
434	433	mpteq2dv	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
435	434	oveq2d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) = ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) )
436	431 435	oveq12d	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( ( b u. a ) |` J ) ) ` ( ( b u. a ) |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( ( b u. a ) |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( ( b u. a ) |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
437	417 436	eqtrid	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> [_ ( b u. a ) / d ]_ ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
438	400 401 402 437	fmpocos	|- ( ph -> ( ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) o. ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) ) = ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) )
439	438	oveq2d	|- ( ph -> ( R gsum ( ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) o. ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) ) ) = ( R gsum ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) )
440		ovex	|- ( NN0 ^m ( I \ J ) ) e. _V
441	440	rabex	|- { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } e. _V
442	441	a1i	|- ( ph -> { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } e. _V )
443	178	a1i	|- ( ph -> { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } e. _V )
444	33	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> R e. Ring )
445	22	ffvelcdmda	|- ( ( ph /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) e. ( Base ` U ) )
446	4 2 12 137 445	mplelf	|- ( ( ph /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) : { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } --> K )
447	446	ffvelcdmda	|- ( ( ( ph /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) /\ b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) e. K )
448	447	an32s	|- ( ( ( ph /\ b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } ) /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) e. K )
449	448	anasss	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) e. K )
450	27	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> J e. _V )
451	8	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> R e. CRing )
452	36	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( A |` J ) e. ( K ^m J ) )
453		simprr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } )
454	20 2 47 49 450 451 452 453	evlsvvvallem	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) e. K )
455	2 136 444 449 454	ringcld	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) e. K )
456	15	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( I \ J ) e. _V )
457	11 14	elmapssresd	|- ( ph -> ( A |` ( I \ J ) ) e. ( K ^m ( I \ J ) ) )
458	457	adantr	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( A |` ( I \ J ) ) e. ( K ^m ( I \ J ) ) )
459		simprl	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } )
460	137 2 47 49 456 451 458 459	evlsvvvallem	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) e. K )
461	2 136 444 455 460	ringcld	|- ( ( ph /\ ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } /\ a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) e. K )
462	461	ralrimivva	|- ( ph -> A. b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } A. a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) e. K )
463	267	fmpo	|- ( A. b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } A. a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) e. K <-> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) --> K )
464	462 463	sylib	|- ( ph -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) --> K )
465		f1of1	|- ( ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -1-1-onto-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
466	368 465	syl	|- ( ph -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) : ( { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } X. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } ) -1-1-> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
467	278	mptex	|- ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e. _V
468	467	a1i	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e. _V )
469	366 466 363 468	fsuppco	|- ( ph -> ( ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) o. ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( b u. a ) ) ) finSupp ( 0g ` R ) )
470	438 469	eqbrtrrd	|- ( ph -> ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) finSupp ( 0g ` R ) )
471	2 197 276 442 443 464 470	gsumxp	|- ( ph -> ( R gsum ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) ) ) )
472	369 439 471	3eqtrd	|- ( ph -> ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( R gsum ( e e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( c ( b e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } , a e. { g e. ( NN0 ^m J ) | ( `' g " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` a ) ` b ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( a ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( b ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) e ) ) ) ) ) )
473	2 136 280 291 322 346	ringassd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) )
474	47 136	mgpplusg	|- ( .r ` R ) = ( +g ` ( mulGrp ` R ) )
475	51	ad2antrr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( mulGrp ` R ) e. Mnd )
476	296	ffvelcdmda	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( d ` i ) e. NN0 )
477	57	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> A : I --> K )
478	477	ffvelcdmda	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( A ` i ) e. K )
479	48 49 475 476 478	mulgnn0cld	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ i e. I ) -> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) e. K )
480	479	fmpttd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) : I --> K )
481	296	feqmptd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d = ( i e. I |-> ( d ` i ) ) )
482	481 309	eqbrtrrd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. I |-> ( d ` i ) ) finSupp 0 )
483	111	adantl	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. K ) -> ( 0 ( .g ` ( mulGrp ` R ) ) k ) = ( 0g ` ( mulGrp ` R ) ) )
484	482 483 476 478 305	fsuppssov1	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) finSupp ( 0g ` ( mulGrp ` R ) ) )
485		disjdif	|- ( J i^i ( I \ J ) ) = (/)
486	485	a1i	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( J i^i ( I \ J ) ) = (/) )
487		undif	|- ( J C_ I <-> ( J u. ( I \ J ) ) = I )
488	9 487	sylib	|- ( ph -> ( J u. ( I \ J ) ) = I )
489	488	eqcomd	|- ( ph -> I = ( J u. ( I \ J ) ) )
490	489	adantr	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I = ( J u. ( I \ J ) ) )
491	48 110 474 292 283 480 484 486 490	gsumsplit	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` ( I \ J ) ) ) ) )
492	284	resmptd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` J ) = ( i e. J |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) )
493		fveq2	|- ( i = j -> ( d ` i ) = ( d ` j ) )
494		fveq2	|- ( i = j -> ( A ` i ) = ( A ` j ) )
495	493 494	oveq12d	|- ( i = j -> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( ( d ` j ) ( .g ` ( mulGrp ` R ) ) ( A ` j ) ) )
496	495	cbvmptv	|- ( i e. J |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) = ( j e. J |-> ( ( d ` j ) ( .g ` ( mulGrp ` R ) ) ( A ` j ) ) )
497		simpr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> j e. J )
498	497	fvresd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( d |` J ) ` j ) = ( d ` j ) )
499	497	fvresd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( A |` J ) ` j ) = ( A ` j ) )
500	498 499	oveq12d	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) = ( ( d ` j ) ( .g ` ( mulGrp ` R ) ) ( A ` j ) ) )
501	500	eqcomd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ j e. J ) -> ( ( d ` j ) ( .g ` ( mulGrp ` R ) ) ( A ` j ) ) = ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) )
502	501	mpteq2dva	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( j e. J |-> ( ( d ` j ) ( .g ` ( mulGrp ` R ) ) ( A ` j ) ) ) = ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
503	496 502	eqtrid	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. J |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) = ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
504	492 503	eqtrd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` J ) = ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) )
505	504	oveq2d	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` J ) ) = ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) )
506	289	resmptd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` ( I \ J ) ) = ( i e. ( I \ J ) |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) )
507		fveq2	|- ( i = k -> ( d ` i ) = ( d ` k ) )
508		fveq2	|- ( i = k -> ( A ` i ) = ( A ` k ) )
509	507 508	oveq12d	|- ( i = k -> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) = ( ( d ` k ) ( .g ` ( mulGrp ` R ) ) ( A ` k ) ) )
510	509	cbvmptv	|- ( i e. ( I \ J ) |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) = ( k e. ( I \ J ) |-> ( ( d ` k ) ( .g ` ( mulGrp ` R ) ) ( A ` k ) ) )
511		simpr	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> k e. ( I \ J ) )
512	511	fvresd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( d |` ( I \ J ) ) ` k ) = ( d ` k ) )
513	511	fvresd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( A |` ( I \ J ) ) ` k ) = ( A ` k ) )
514	512 513	oveq12d	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) = ( ( d ` k ) ( .g ` ( mulGrp ` R ) ) ( A ` k ) ) )
515	514	eqcomd	|- ( ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) /\ k e. ( I \ J ) ) -> ( ( d ` k ) ( .g ` ( mulGrp ` R ) ) ( A ` k ) ) = ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) )
516	515	mpteq2dva	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( k e. ( I \ J ) |-> ( ( d ` k ) ( .g ` ( mulGrp ` R ) ) ( A ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
517	510 516	eqtrid	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( i e. ( I \ J ) |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) = ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
518	506 517	eqtrd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` ( I \ J ) ) = ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) )
519	518	oveq2d	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` ( I \ J ) ) ) = ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) )
520	505 519	oveq12d	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` J ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) |` ( I \ J ) ) ) ) = ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) )
521	491 520	eqtr2d	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) )
522	351 521	oveq12d	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) = ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) )
523	473 522	eqtrd	|- ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) = ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) )
524	523	mpteq2dva	|- ( ph -> ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) = ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) )
525	524	oveq2d	|- ( ph -> ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( d |` J ) ) ` ( d |` ( I \ J ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( j e. J |-> ( ( ( d |` J ) ` j ) ( .g ` ( mulGrp ` R ) ) ( ( A |` J ) ` j ) ) ) ) ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( ( d |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) )
526	275 472 525	3eqtr2d	|- ( ph -> ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) = ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) )
527		eqid	|- ( ( I \ J ) eval R ) = ( ( I \ J ) eval R )
528	527 4 12 137 2 47 49 136 15 8 166 457	evlvvval	|- ( ph -> ( ( ( ( I \ J ) eval R ) ` ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ) ` ( A |` ( I \ J ) ) ) = ( R gsum ( c e. { f e. ( NN0 ^m ( I \ J ) ) | ( `' f " NN ) e. Fin } |-> ( ( ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ` c ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( k e. ( I \ J ) |-> ( ( c ` k ) ( .g ` ( mulGrp ` R ) ) ( ( A |` ( I \ J ) ) ` k ) ) ) ) ) ) ) )
529		eqid	|- ( I eval R ) = ( I eval R )
530	529 1 3 282 2 47 49 136 7 8 10 11	evlvvval	|- ( ph -> ( ( ( I eval R ) ` F ) ` A ) = ( R gsum ( d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( ( F ` d ) ( .r ` R ) ( ( mulGrp ` R ) gsum ( i e. I |-> ( ( d ` i ) ( .g ` ( mulGrp ` R ) ) ( A ` i ) ) ) ) ) ) ) )
531	526 528 530	3eqtr4d	|- ( ph -> ( ( ( ( I \ J ) eval R ) ` ( ( ( J eval U ) ` ( ( ( I selectVars R ) ` J ) ` F ) ) ` ( L o. ( A |` J ) ) ) ) ` ( A |` ( I \ J ) ) ) = ( ( ( I eval R ) ` F ) ` A ) )