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

Metamath Proof Explorer

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