Metamath Proof Explorer

Theorem selvvvval

Description: Recover the original polynomial from a selectVars application. (Contributed by SN, 15-Mar-2025)

Ref Expression
Hypotheses selvvvval.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
selvvvval.p 
|- P = ( I mPoly R )
selvvvval.b 
|- B = ( Base ` P )
selvvvval.r 
|- ( ph -> R e. CRing )
selvvvval.j 
|- ( ph -> J C_ I )
selvvvval.f 
|- ( ph -> F e. B )
selvvvval.y 
|- ( ph -> Y e. D )
Assertion selvvvval 
|- ( ph -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = ( F ` Y ) )

Proof

Step Hyp Ref Expression
1 selvvvval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 selvvvval.p 
 |-  P = ( I mPoly R )
3 selvvvval.b 
 |-  B = ( Base ` P )
4 selvvvval.r 
 |-  ( ph -> R e. CRing )
5 selvvvval.j 
 |-  ( ph -> J C_ I )
6 selvvvval.f 
 |-  ( ph -> F e. B )
7 selvvvval.y 
 |-  ( ph -> Y e. D )
8 eqid 
 |-  ( ( I \ J ) mPoly R ) = ( ( I \ J ) mPoly R )
9 eqid 
 |-  ( J mPoly ( ( I \ J ) mPoly R ) ) = ( J mPoly ( ( I \ J ) mPoly R ) )
10 eqid 
 |-  ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
11 eqid 
 |-  ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) )
12 2 3 8 9 10 11 4 5 6 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( I eval ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ) ` ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ) )
13 eqid 
 |-  ( I eval ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( I eval ( J mPoly ( ( I \ J ) mPoly R ) ) )
14 eqid 
 |-  ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) )
15 eqid 
 |-  ( Base ` ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( Base ` ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
16 eqid 
 |-  ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
17 eqid 
 |-  ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
18 eqid 
 |-  ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
19 eqid 
 |-  ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
20 2 3 mplrcl 
 |-  ( F e. B -> I e. _V )
21 6 20 syl 
 |-  ( ph -> I e. _V )
22 21 5 ssexd 
 |-  ( ph -> J e. _V )
23 21 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
24 8 23 4 mplcrngd 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. CRing )
25 9 22 24 mplcrngd 
 |-  ( ph -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. CRing )
26 9 mplassa 
 |-  ( ( J e. _V /\ ( ( I \ J ) mPoly R ) e. CRing ) -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg )
27 22 24 26 syl2anc 
 |-  ( ph -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg )
28 eqid 
 |-  ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
29 10 28 asclrhm 
 |-  ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
30 27 29 syl 
 |-  ( ph -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
31 8 mplassa 
 |-  ( ( ( I \ J ) e. _V /\ R e. CRing ) -> ( ( I \ J ) mPoly R ) e. AssAlg )
32 23 4 31 syl2anc 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. AssAlg )
33 eqid 
 |-  ( algSc ` ( ( I \ J ) mPoly R ) ) = ( algSc ` ( ( I \ J ) mPoly R ) )
34 eqid 
 |-  ( Scalar ` ( ( I \ J ) mPoly R ) ) = ( Scalar ` ( ( I \ J ) mPoly R ) )
35 33 34 asclrhm 
 |-  ( ( ( I \ J ) mPoly R ) e. AssAlg -> ( algSc ` ( ( I \ J ) mPoly R ) ) e. ( ( Scalar ` ( ( I \ J ) mPoly R ) ) RingHom ( ( I \ J ) mPoly R ) ) )
36 32 35 syl 
 |-  ( ph -> ( algSc ` ( ( I \ J ) mPoly R ) ) e. ( ( Scalar ` ( ( I \ J ) mPoly R ) ) RingHom ( ( I \ J ) mPoly R ) ) )
37 8 23 4 mplsca 
 |-  ( ph -> R = ( Scalar ` ( ( I \ J ) mPoly R ) ) )
38 37 eqcomd 
 |-  ( ph -> ( Scalar ` ( ( I \ J ) mPoly R ) ) = R )
39 9 22 24 mplsca 
 |-  ( ph -> ( ( I \ J ) mPoly R ) = ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
40 38 39 oveq12d 
 |-  ( ph -> ( ( Scalar ` ( ( I \ J ) mPoly R ) ) RingHom ( ( I \ J ) mPoly R ) ) = ( R RingHom ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
41 36 40 eleqtrd 
 |-  ( ph -> ( algSc ` ( ( I \ J ) mPoly R ) ) e. ( R RingHom ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
42 rhmco 
 |-  ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) /\ ( algSc ` ( ( I \ J ) mPoly R ) ) e. ( R RingHom ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
43 30 41 42 syl2anc 
 |-  ( ph -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
44 rhmghm 
 |-  ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R GrpHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
45 ghmmhm 
 |-  ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R GrpHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R MndHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
46 43 44 45 3syl 
 |-  ( ph -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) e. ( R MndHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
47 2 14 3 15 46 6 mhmcompl 
 |-  ( ph -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) e. ( Base ` ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
48 fvexd 
 |-  ( ph -> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. _V )
49 eqid 
 |-  ( J mVar ( ( I \ J ) mPoly R ) ) = ( J mVar ( ( I \ J ) mPoly R ) )
50 24 crngringd 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. Ring )
51 9 49 16 22 50 mvrf2 
 |-  ( ph -> ( J mVar ( ( I \ J ) mPoly R ) ) : J --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
52 51 ffvelcdmda 
 |-  ( ( ph /\ z e. J ) -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
53 52 adantlr 
 |-  ( ( ( ph /\ z e. I ) /\ z e. J ) -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
54 eldif 
 |-  ( z e. ( I \ J ) <-> ( z e. I /\ -. z e. J ) )
55 eqid 
 |-  ( Base ` ( ( I \ J ) mPoly R ) ) = ( Base ` ( ( I \ J ) mPoly R ) )
56 9 16 55 10 22 50 mplasclf 
 |-  ( ph -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) : ( Base ` ( ( I \ J ) mPoly R ) ) --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
57 56 adantr 
 |-  ( ( ph /\ z e. ( I \ J ) ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) : ( Base ` ( ( I \ J ) mPoly R ) ) --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
58 eqid 
 |-  ( ( I \ J ) mVar R ) = ( ( I \ J ) mVar R )
59 4 crngringd 
 |-  ( ph -> R e. Ring )
60 8 58 55 23 59 mvrf2 
 |-  ( ph -> ( ( I \ J ) mVar R ) : ( I \ J ) --> ( Base ` ( ( I \ J ) mPoly R ) ) )
61 60 ffvelcdmda 
 |-  ( ( ph /\ z e. ( I \ J ) ) -> ( ( ( I \ J ) mVar R ) ` z ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
62 57 61 ffvelcdmd 
 |-  ( ( ph /\ z e. ( I \ J ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
63 54 62 sylan2br 
 |-  ( ( ph /\ ( z e. I /\ -. z e. J ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
64 63 anassrs 
 |-  ( ( ( ph /\ z e. I ) /\ -. z e. J ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
65 53 64 ifclda 
 |-  ( ( ph /\ z e. I ) -> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
66 65 fmpttd 
 |-  ( ph -> ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) : I --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
67 48 21 66 elmapdd 
 |-  ( ph -> ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) e. ( ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ^m I ) )
68 13 14 15 1 16 17 18 19 21 25 47 67 evlvvval 
 |-  ( ph -> ( ( ( I eval ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ) ` ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ) = ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) ) ) ) )
69 eqid 
 |-  ( Base ` R ) = ( Base ` R )
70 2 69 3 1 6 mplelf 
 |-  ( ph -> F : D --> ( Base ` R ) )
71 70 adantr 
 |-  ( ( ph /\ g e. D ) -> F : D --> ( Base ` R ) )
72 simpr 
 |-  ( ( ph /\ g e. D ) -> g e. D )
73 71 72 fvco3d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) = ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) ` ( F ` g ) ) )
74 8 55 69 33 23 59 mplasclf 
 |-  ( ph -> ( algSc ` ( ( I \ J ) mPoly R ) ) : ( Base ` R ) --> ( Base ` ( ( I \ J ) mPoly R ) ) )
75 74 adantr 
 |-  ( ( ph /\ g e. D ) -> ( algSc ` ( ( I \ J ) mPoly R ) ) : ( Base ` R ) --> ( Base ` ( ( I \ J ) mPoly R ) ) )
76 70 ffvelcdmda 
 |-  ( ( ph /\ g e. D ) -> ( F ` g ) e. ( Base ` R ) )
77 75 76 fvco3d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) ` ( F ` g ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) )
78 73 77 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) )
79 17 16 mgpbas 
 |-  ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( Base ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
80 eqid 
 |-  ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
81 17 19 mgpplusg 
 |-  ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( +g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
82 17 crngmgp 
 |-  ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. CRing -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. CMnd )
83 25 82 syl 
 |-  ( ph -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. CMnd )
84 83 adantr 
 |-  ( ( ph /\ g e. D ) -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. CMnd )
85 21 adantr 
 |-  ( ( ph /\ g e. D ) -> I e. _V )
86 83 cmnmndd 
 |-  ( ph -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. Mnd )
87 86 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. Mnd )
88 1 psrbagf 
 |-  ( g e. D -> g : I --> NN0 )
89 88 adantl 
 |-  ( ( ph /\ g e. D ) -> g : I --> NN0 )
90 89 ffvelcdmda 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( g ` k ) e. NN0 )
91 eqid 
 |-  ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) = ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) )
92 eleq1w 
 |-  ( z = k -> ( z e. J <-> k e. J ) )
93 fveq2 
 |-  ( z = k -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) = ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) )
94 fveq2 
 |-  ( z = k -> ( ( ( I \ J ) mVar R ) ` z ) = ( ( ( I \ J ) mVar R ) ` k ) )
95 94 fveq2d 
 |-  ( z = k -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) )
96 92 93 95 ifbieq12d 
 |-  ( z = k -> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) = if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
97 simpr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> k e. I )
98 51 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( J mVar ( ( I \ J ) mPoly R ) ) : J --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
99 98 ffvelcdmda 
 |-  ( ( ( ( ph /\ g e. D ) /\ k e. I ) /\ k e. J ) -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
100 eldif 
 |-  ( k e. ( I \ J ) <-> ( k e. I /\ -. k e. J ) )
101 56 adantr 
 |-  ( ( ph /\ k e. ( I \ J ) ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) : ( Base ` ( ( I \ J ) mPoly R ) ) --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
102 60 ffvelcdmda 
 |-  ( ( ph /\ k e. ( I \ J ) ) -> ( ( ( I \ J ) mVar R ) ` k ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
103 101 102 ffvelcdmd 
 |-  ( ( ph /\ k e. ( I \ J ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
104 100 103 sylan2br 
 |-  ( ( ph /\ ( k e. I /\ -. k e. J ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
105 104 anassrs 
 |-  ( ( ( ph /\ k e. I ) /\ -. k e. J ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
106 105 adantllr 
 |-  ( ( ( ( ph /\ g e. D ) /\ k e. I ) /\ -. k e. J ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
107 99 106 ifclda 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
108 91 96 97 107 fvmptd3 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) = if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
109 108 107 eqeltrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
110 79 18 87 90 109 mulgnn0cld 
 |-  ( ( ( ph /\ g e. D ) /\ k e. I ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
111 110 fmpttd 
 |-  ( ( ph /\ g e. D ) -> ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) : I --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
112 89 feqmptd 
 |-  ( ( ph /\ g e. D ) -> g = ( k e. I |-> ( g ` k ) ) )
113 1 psrbagfsupp 
 |-  ( g e. D -> g finSupp 0 )
114 113 adantl 
 |-  ( ( ph /\ g e. D ) -> g finSupp 0 )
115 112 114 eqbrtrrd 
 |-  ( ( ph /\ g e. D ) -> ( k e. I |-> ( g ` k ) ) finSupp 0 )
116 79 80 18 mulg0 
 |-  ( t e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) -> ( 0 ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) t ) = ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
117 116 adantl 
 |-  ( ( ( ph /\ g e. D ) /\ t e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( 0 ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) t ) = ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
118 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) e. _V )
119 115 117 90 109 118 fsuppssov1 
 |-  ( ( ph /\ g e. D ) -> ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
120 disjdifr 
 |-  ( ( I \ J ) i^i J ) = (/)
121 120 a1i 
 |-  ( ( ph /\ g e. D ) -> ( ( I \ J ) i^i J ) = (/) )
122 undifr 
 |-  ( J C_ I <-> ( ( I \ J ) u. J ) = I )
123 5 122 sylib 
 |-  ( ph -> ( ( I \ J ) u. J ) = I )
124 123 eqcomd 
 |-  ( ph -> I = ( ( I \ J ) u. J ) )
125 124 adantr 
 |-  ( ( ph /\ g e. D ) -> I = ( ( I \ J ) u. J ) )
126 79 80 81 84 85 111 119 121 125 gsumsplit 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) = ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` J ) ) ) )
127 eldifi 
 |-  ( k e. ( I \ J ) -> k e. I )
128 127 adantl 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> k e. I )
129 127 107 sylan2 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
130 91 96 128 129 fvmptd3 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) = if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
131 eldifn 
 |-  ( k e. ( I \ J ) -> -. k e. J )
132 131 adantl 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> -. k e. J )
133 132 iffalsed 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) )
134 130 133 eqtrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) )
135 134 oveq2d 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
136 eqid 
 |-  ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
137 136 17 rhmmhm 
 |-  ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) RingHom ( J mPoly ( ( I \ J ) mPoly R ) ) ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) MndHom ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
138 30 137 syl 
 |-  ( ph -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) MndHom ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
139 138 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) MndHom ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
140 127 90 sylan2 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( g ` k ) e. NN0 )
141 102 adantlr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( ( I \ J ) mVar R ) ` k ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
142 39 fveq2d 
 |-  ( ph -> ( Base ` ( ( I \ J ) mPoly R ) ) = ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
143 142 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( Base ` ( ( I \ J ) mPoly R ) ) = ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
144 141 143 eleqtrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( ( I \ J ) mVar R ) ` k ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
145 eqid 
 |-  ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
146 136 145 mgpbas 
 |-  ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( Base ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
147 eqid 
 |-  ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) = ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
148 146 147 18 mhmmulg 
 |-  ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) MndHom ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) /\ ( g ` k ) e. NN0 /\ ( ( ( I \ J ) mVar R ) ` k ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
149 139 140 144 148 syl3anc 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
150 135 149 eqtr4d 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) )
151 150 mpteq2dva 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
152 difssd 
 |-  ( ( ph /\ g e. D ) -> ( I \ J ) C_ I )
153 152 resmptd 
 |-  ( ( ph /\ g e. D ) -> ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) = ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) )
154 56 adantr 
 |-  ( ( ph /\ g e. D ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) : ( Base ` ( ( I \ J ) mPoly R ) ) --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
155 39 fveq2d 
 |-  ( ph -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) = ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
156 155 fveq2d 
 |-  ( ph -> ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) = ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) )
157 156 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) = ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) )
158 157 oveqd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) )
159 eqid 
 |-  ( mulGrp ` ( ( I \ J ) mPoly R ) ) = ( mulGrp ` ( ( I \ J ) mPoly R ) )
160 159 55 mgpbas 
 |-  ( Base ` ( ( I \ J ) mPoly R ) ) = ( Base ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) )
161 eqid 
 |-  ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) = ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) )
162 159 crngmgp 
 |-  ( ( ( I \ J ) mPoly R ) e. CRing -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) e. CMnd )
163 24 162 syl 
 |-  ( ph -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) e. CMnd )
164 163 cmnmndd 
 |-  ( ph -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) e. Mnd )
165 164 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) e. Mnd )
166 160 161 165 140 141 mulgnn0cld 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
167 158 166 eqeltrrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
168 154 167 cofmpt 
 |-  ( ( ph /\ g e. D ) -> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) = ( k e. ( I \ J ) |-> ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
169 151 153 168 3eqtr4d 
 |-  ( ( ph /\ g e. D ) -> ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
170 169 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) ) = ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) )
171 eqid 
 |-  ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) = ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
172 39 24 eqeltrrd 
 |-  ( ph -> ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. CRing )
173 136 crngmgp 
 |-  ( ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. CRing -> ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) e. CMnd )
174 172 173 syl 
 |-  ( ph -> ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) e. CMnd )
175 174 adantr 
 |-  ( ( ph /\ g e. D ) -> ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) e. CMnd )
176 86 adantr 
 |-  ( ( ph /\ g e. D ) -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. Mnd )
177 23 adantr 
 |-  ( ( ph /\ g e. D ) -> ( I \ J ) e. _V )
178 138 adantr 
 |-  ( ( ph /\ g e. D ) -> ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) MndHom ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
179 167 143 eleqtrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
180 179 fmpttd 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) : ( I \ J ) --> ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
181 0zd 
 |-  ( ( ph /\ g e. D ) -> 0 e. ZZ )
182 115 152 181 fmptssfisupp 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( g ` k ) ) finSupp 0 )
183 142 eqimssd 
 |-  ( ph -> ( Base ` ( ( I \ J ) mPoly R ) ) C_ ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
184 183 sselda 
 |-  ( ( ph /\ u e. ( Base ` ( ( I \ J ) mPoly R ) ) ) -> u e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
185 184 adantlr 
 |-  ( ( ( ph /\ g e. D ) /\ u e. ( Base ` ( ( I \ J ) mPoly R ) ) ) -> u e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
186 146 171 147 mulg0 
 |-  ( u e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( 0 ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) u ) = ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) )
187 185 186 syl 
 |-  ( ( ( ph /\ g e. D ) /\ u e. ( Base ` ( ( I \ J ) mPoly R ) ) ) -> ( 0 ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) u ) = ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) )
188 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) e. _V )
189 182 187 140 141 188 fsuppssov1 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) )
190 146 171 175 176 177 178 180 189 gsummhm 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) )
191 170 190 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) ) = ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) )
192 5 adantr 
 |-  ( ( ph /\ g e. D ) -> J C_ I )
193 192 resmptd 
 |-  ( ( ph /\ g e. D ) -> ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` J ) = ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) )
194 192 sselda 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> k e. I )
195 194 107 syldan 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
196 91 96 194 195 fvmptd3 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) = if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) )
197 iftrue 
 |-  ( k e. J -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) )
198 197 adantl 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> if ( k e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) )
199 196 198 eqtrd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) = ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) )
200 199 oveq2d 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) )
201 200 mpteq2dva 
 |-  ( ( ph /\ g e. D ) -> ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) = ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) )
202 193 201 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` J ) = ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) )
203 202 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` J ) ) = ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) )
204 191 203 oveq12d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` ( I \ J ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) |` J ) ) ) = ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
205 27 adantr 
 |-  ( ( ph /\ g e. D ) -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg )
206 146 171 175 177 180 189 gsumcl 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
207 22 adantr 
 |-  ( ( ph /\ g e. D ) -> J e. _V )
208 86 ad2antrr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. Mnd )
209 194 90 syldan 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( g ` k ) e. NN0 )
210 51 ffvelcdmda 
 |-  ( ( ph /\ k e. J ) -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
211 210 adantlr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
212 79 18 208 209 211 mulgnn0cld 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
213 212 fmpttd 
 |-  ( ( ph /\ g e. D ) -> ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) : J --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
214 115 192 181 fmptssfisupp 
 |-  ( ( ph /\ g e. D ) -> ( k e. J |-> ( g ` k ) ) finSupp 0 )
215 214 117 209 211 118 fsuppssov1 
 |-  ( ( ph /\ g e. D ) -> ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
216 79 80 84 207 213 215 gsumcl 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
217 eqid 
 |-  ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
218 10 28 145 16 19 217 asclmul1 
 |-  ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg /\ ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) /\ ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
219 205 206 216 218 syl3anc 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
220 156 oveqd 
 |-  ( ph -> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) )
221 220 mpteq2dv 
 |-  ( ph -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) )
222 155 221 oveq12d 
 |-  ( ph -> ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) = ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
223 222 adantr 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) = ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
224 223 oveq1d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) = ( ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
225 219 224 eqtr4d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) = ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
226 126 204 225 3eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) = ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) )
227 78 226 oveq12d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) ) = ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) )
228 75 76 ffvelcdmd 
 |-  ( ( ph /\ g e. D ) -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
229 142 adantr 
 |-  ( ( ph /\ g e. D ) -> ( Base ` ( ( I \ J ) mPoly R ) ) = ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
230 228 229 eleqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
231 9 22 50 mpllmodd 
 |-  ( ph -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. LMod )
232 231 adantr 
 |-  ( ( ph /\ g e. D ) -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. LMod )
233 eqid 
 |-  ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) = ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) )
234 163 adantr 
 |-  ( ( ph /\ g e. D ) -> ( mulGrp ` ( ( I \ J ) mPoly R ) ) e. CMnd )
235 166 fmpttd 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) : ( I \ J ) --> ( Base ` ( ( I \ J ) mPoly R ) ) )
236 160 233 161 mulg0 
 |-  ( e e. ( Base ` ( ( I \ J ) mPoly R ) ) -> ( 0 ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) e ) = ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) )
237 236 adantl 
 |-  ( ( ( ph /\ g e. D ) /\ e e. ( Base ` ( ( I \ J ) mPoly R ) ) ) -> ( 0 ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) e ) = ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) )
238 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) e. _V )
239 182 237 140 141 238 fsuppssov1 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) finSupp ( 0g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) )
240 160 233 234 177 235 239 gsumcl 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
241 240 229 eleqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
242 16 28 217 145 232 241 216 lmodvscld 
 |-  ( ( ph /\ g e. D ) -> ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
243 10 28 145 16 19 217 asclmul1 
 |-  ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. AssAlg /\ ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) e. ( Base ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) /\ ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) )
244 205 230 242 243 syl3anc 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) )
245 227 244 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) ) = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) )
246 245 mpteq2dva 
 |-  ( ph -> ( g e. D |-> ( ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) ) ) = ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) )
247 246 oveq2d 
 |-  ( ph -> ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) o. ( algSc ` ( ( I \ J ) mPoly R ) ) ) o. F ) ` g ) ( .r ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. I |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( z e. I |-> if ( z e. J , ( ( J mVar ( ( I \ J ) mPoly R ) ) ` z ) , ( ( algSc ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ` ( ( ( I \ J ) mVar R ) ` z ) ) ) ) ` k ) ) ) ) ) ) ) = ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) )
248 12 68 247 3eqtrd 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) )
249 248 fveq1d 
 |-  ( ph -> ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( Y |` J ) ) = ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) )
250 249 fveq1d 
 |-  ( ph -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = ( ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) )
251 eqid 
 |-  ( 0g ` ( ( I \ J ) mPoly R ) ) = ( 0g ` ( ( I \ J ) mPoly R ) )
252 50 ringcmnd 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. CMnd )
253 4 crnggrpd 
 |-  ( ph -> R e. Grp )
254 253 grpmndd 
 |-  ( ph -> R e. Mnd )
255 ovex 
 |-  ( NN0 ^m I ) e. _V
256 1 255 rabex2 
 |-  D e. _V
257 256 a1i 
 |-  ( ph -> D e. _V )
258 eqid 
 |-  { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } = { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin }
259 eqid 
 |-  ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) = ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) )
260 difssd 
 |-  ( ph -> ( I \ J ) C_ I )
261 1 258 21 260 7 psrbagres 
 |-  ( ph -> ( Y |` ( I \ J ) ) e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } )
262 8 55 258 259 23 253 261 mplmapghm 
 |-  ( ph -> ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) e. ( ( ( I \ J ) mPoly R ) GrpHom R ) )
263 ghmmhm 
 |-  ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) e. ( ( ( I \ J ) mPoly R ) GrpHom R ) -> ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) e. ( ( ( I \ J ) mPoly R ) MndHom R ) )
264 262 263 syl 
 |-  ( ph -> ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) e. ( ( ( I \ J ) mPoly R ) MndHom R ) )
265 eqid 
 |-  { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin }
266 simpr 
 |-  ( ( ph /\ w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
267 9 55 16 265 266 mplelf 
 |-  ( ( ph /\ w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> w : { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } --> ( Base ` ( ( I \ J ) mPoly R ) ) )
268 1 265 21 5 7 psrbagres 
 |-  ( ph -> ( Y |` J ) e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } )
269 268 adantr 
 |-  ( ( ph /\ w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( Y |` J ) e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } )
270 267 269 ffvelcdmd 
 |-  ( ( ph /\ w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( w ` ( Y |` J ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
271 270 fmpttd 
 |-  ( ph -> ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) : ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) --> ( Base ` ( ( I \ J ) mPoly R ) ) )
272 16 28 217 145 232 230 242 lmodvscld 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
273 272 fmpttd 
 |-  ( ph -> ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) : D --> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
274 271 273 fcod 
 |-  ( ph -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) : D --> ( Base ` ( ( I \ J ) mPoly R ) ) )
275 fvexd 
 |-  ( ph -> ( 0g ` ( ( I \ J ) mPoly R ) ) e. _V )
276 25 crngringd 
 |-  ( ph -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. Ring )
277 eqid 
 |-  ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) = ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) )
278 16 277 ring0cl 
 |-  ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. Ring -> ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
279 276 278 syl 
 |-  ( ph -> ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
280 ssidd 
 |-  ( ph -> ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) C_ ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
281 256 mptex 
 |-  ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) e. _V
282 281 a1i 
 |-  ( ph -> ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) e. _V )
283 fvexd 
 |-  ( ph -> ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) e. _V )
284 funmpt 
 |-  Fun ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) )
285 284 a1i 
 |-  ( ph -> Fun ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) )
286 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
287 2 3 286 6 4 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
288 ssidd 
 |-  ( ph -> ( F supp ( 0g ` R ) ) C_ ( F supp ( 0g ` R ) ) )
289 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
290 70 288 6 289 suppssrg 
 |-  ( ( ph /\ g e. ( D \ ( F supp ( 0g ` R ) ) ) ) -> ( F ` g ) = ( 0g ` R ) )
291 290 fveq2d 
 |-  ( ( ph /\ g e. ( D \ ( F supp ( 0g ` R ) ) ) ) -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) = ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( 0g ` R ) ) )
292 8 33 286 251 23 59 mplascl0 
 |-  ( ph -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( 0g ` R ) ) = ( 0g ` ( ( I \ J ) mPoly R ) ) )
293 39 fveq2d 
 |-  ( ph -> ( 0g ` ( ( I \ J ) mPoly R ) ) = ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
294 292 293 eqtrd 
 |-  ( ph -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( 0g ` R ) ) = ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
295 294 adantr 
 |-  ( ( ph /\ g e. ( D \ ( F supp ( 0g ` R ) ) ) ) -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( 0g ` R ) ) = ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
296 291 295 eqtrd 
 |-  ( ( ph /\ g e. ( D \ ( F supp ( 0g ` R ) ) ) ) -> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) = ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
297 296 257 suppss2 
 |-  ( ph -> ( ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) supp ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ) C_ ( F supp ( 0g ` R ) ) )
298 282 283 285 287 297 fsuppsssuppgd 
 |-  ( ph -> ( g e. D |-> ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ) finSupp ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) )
299 eqid 
 |-  ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
300 16 28 217 299 277 lmod0vs 
 |-  ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) e. LMod /\ f e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) f ) = ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
301 231 300 sylan 
 |-  ( ( ph /\ f e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) -> ( ( 0g ` ( Scalar ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) f ) = ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
302 fvexd 
 |-  ( ph -> ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) e. _V )
303 298 301 228 242 302 fsuppssov1 
 |-  ( ph -> ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) finSupp ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
304 eqid 
 |-  ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) = ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) )
305 24 crnggrpd 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. Grp )
306 9 16 265 304 22 305 268 mplmapghm 
 |-  ( ph -> ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) e. ( ( J mPoly ( ( I \ J ) mPoly R ) ) GrpHom ( ( I \ J ) mPoly R ) ) )
307 ghmmhm 
 |-  ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) e. ( ( J mPoly ( ( I \ J ) mPoly R ) ) GrpHom ( ( I \ J ) mPoly R ) ) -> ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) e. ( ( J mPoly ( ( I \ J ) mPoly R ) ) MndHom ( ( I \ J ) mPoly R ) ) )
308 306 307 syl 
 |-  ( ph -> ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) e. ( ( J mPoly ( ( I \ J ) mPoly R ) ) MndHom ( ( I \ J ) mPoly R ) ) )
309 277 251 mhm0 
 |-  ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) e. ( ( J mPoly ( ( I \ J ) mPoly R ) ) MndHom ( ( I \ J ) mPoly R ) ) -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) ` ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( 0g ` ( ( I \ J ) mPoly R ) ) )
310 308 309 syl 
 |-  ( ph -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) ` ( 0g ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) = ( 0g ` ( ( I \ J ) mPoly R ) ) )
311 275 279 273 271 280 257 48 303 310 fsuppcor 
 |-  ( ph -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) finSupp ( 0g ` ( ( I \ J ) mPoly R ) ) )
312 55 251 252 254 257 264 274 311 gsummhm 
 |-  ( ph -> ( R gsum ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) = ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) ` ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) )
313 fveq1 
 |-  ( v = ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) -> ( v ` ( Y |` ( I \ J ) ) ) = ( ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ` ( Y |` ( I \ J ) ) ) )
314 55 251 252 257 274 311 gsumcl 
 |-  ( ph -> ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
315 fvexd 
 |-  ( ph -> ( ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ` ( Y |` ( I \ J ) ) ) e. _V )
316 259 313 314 315 fvmptd3 
 |-  ( ph -> ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) ` ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) = ( ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ` ( Y |` ( I \ J ) ) ) )
317 276 ringcmnd 
 |-  ( ph -> ( J mPoly ( ( I \ J ) mPoly R ) ) e. CMnd )
318 305 grpmndd 
 |-  ( ph -> ( ( I \ J ) mPoly R ) e. Mnd )
319 16 277 317 318 257 308 273 303 gsummhm 
 |-  ( ph -> ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) = ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) ` ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) )
320 fveq1 
 |-  ( w = ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) -> ( w ` ( Y |` J ) ) = ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) )
321 16 277 317 257 273 303 gsumcl 
 |-  ( ph -> ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) )
322 fvexd 
 |-  ( ph -> ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) e. _V )
323 304 320 321 322 fvmptd3 
 |-  ( ph -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) ` ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) = ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) )
324 319 323 eqtrd 
 |-  ( ph -> ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) = ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) )
325 324 fveq1d 
 |-  ( ph -> ( ( ( ( I \ J ) mPoly R ) gsum ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ` ( Y |` ( I \ J ) ) ) = ( ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) )
326 312 316 325 3eqtrrd 
 |-  ( ph -> ( ( ( ( J mPoly ( ( I \ J ) mPoly R ) ) gsum ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = ( R gsum ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) )
327 9 55 16 265 272 mplelf 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) : { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } --> ( Base ` ( ( I \ J ) mPoly R ) ) )
328 268 adantr 
 |-  ( ( ph /\ g e. D ) -> ( Y |` J ) e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } )
329 327 328 ffvelcdmd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
330 eqidd 
 |-  ( ph -> ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) = ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) )
331 eqidd 
 |-  ( ph -> ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) = ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) )
332 fveq1 
 |-  ( w = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) -> ( w ` ( Y |` J ) ) = ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) )
333 272 330 331 332 fmptco 
 |-  ( ph -> ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) = ( g e. D |-> ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ) )
334 eqidd 
 |-  ( ph -> ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) = ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) )
335 fveq1 
 |-  ( v = ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) -> ( v ` ( Y |` ( I \ J ) ) ) = ( ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) )
336 329 333 334 335 fmptco 
 |-  ( ph -> ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) = ( g e. D |-> ( ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) ) )
337 eqid 
 |-  ( .r ` ( ( I \ J ) mPoly R ) ) = ( .r ` ( ( I \ J ) mPoly R ) )
338 9 217 55 16 337 265 228 242 328 mplvscaval 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ` ( Y |` J ) ) ) )
339 9 217 55 16 337 265 240 216 328 mplvscaval 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ` ( Y |` J ) ) = ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) )
340 339 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ` ( Y |` J ) ) ) = ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) )
341 32 adantr 
 |-  ( ( ph /\ g e. D ) -> ( ( I \ J ) mPoly R ) e. AssAlg )
342 37 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) ) )
343 342 adantr 
 |-  ( ( ph /\ g e. D ) -> ( Base ` R ) = ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) ) )
344 76 343 eleqtrd 
 |-  ( ( ph /\ g e. D ) -> ( F ` g ) e. ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) ) )
345 50 adantr 
 |-  ( ( ph /\ g e. D ) -> ( ( I \ J ) mPoly R ) e. Ring )
346 9 55 16 265 216 mplelf 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) : { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } --> ( Base ` ( ( I \ J ) mPoly R ) ) )
347 346 328 ffvelcdmd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
348 55 337 345 240 347 ringcld 
 |-  ( ( ph /\ g e. D ) -> ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
349 eqid 
 |-  ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) ) = ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) )
350 eqid 
 |-  ( .s ` ( ( I \ J ) mPoly R ) ) = ( .s ` ( ( I \ J ) mPoly R ) )
351 33 34 349 55 337 350 asclmul1 
 |-  ( ( ( ( I \ J ) mPoly R ) e. AssAlg /\ ( F ` g ) e. ( Base ` ( Scalar ` ( ( I \ J ) mPoly R ) ) ) /\ ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) ) -> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) = ( ( F ` g ) ( .s ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) )
352 341 344 348 351 syl3anc 
 |-  ( ( ph /\ g e. D ) -> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) = ( ( F ` g ) ( .s ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) )
353 338 340 352 3eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) = ( ( F ` g ) ( .s ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) )
354 353 fveq1d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = ( ( ( F ` g ) ( .s ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) ` ( Y |` ( I \ J ) ) ) )
355 eqid 
 |-  ( .r ` R ) = ( .r ` R )
356 261 adantr 
 |-  ( ( ph /\ g e. D ) -> ( Y |` ( I \ J ) ) e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } )
357 8 350 69 55 355 258 76 348 356 mplvscaval 
 |-  ( ( ph /\ g e. D ) -> ( ( ( F ` g ) ( .s ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ) ` ( Y |` ( I \ J ) ) ) = ( ( F ` g ) ( .r ` R ) ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ` ( Y |` ( I \ J ) ) ) ) )
358 ovif2 
 |-  ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) = if ( ( Y |` J ) = ( g |` J ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) )
359 358 fveq1i 
 |-  ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) = ( if ( ( Y |` J ) = ( g |` J ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) )
360 iffv 
 |-  ( if ( ( Y |` J ) = ( g |` J ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) , ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) = if ( ( Y |` J ) = ( g |` J ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) )
361 359 360 eqtri 
 |-  ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) = if ( ( Y |` J ) = ( g |` J ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) )
362 eqeq1 
 |-  ( i = ( Y |` ( I \ J ) ) -> ( i = ( g |` ( I \ J ) ) <-> ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) )
363 362 ifbid 
 |-  ( i = ( Y |` ( I \ J ) ) -> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
364 eqid 
 |-  ( 1r ` ( ( I \ J ) mPoly R ) ) = ( 1r ` ( ( I \ J ) mPoly R ) )
365 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
366 59 adantr 
 |-  ( ( ph /\ g e. D ) -> R e. Ring )
367 1 258 85 152 72 psrbagres 
 |-  ( ( ph /\ g e. D ) -> ( g |` ( I \ J ) ) e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } )
368 8 55 286 365 258 177 366 367 mplmon 
 |-  ( ( ph /\ g e. D ) -> ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` ( ( I \ J ) mPoly R ) ) )
369 55 337 364 345 368 ringridmd 
 |-  ( ( ph /\ g e. D ) -> ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) = ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
370 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 1r ` R ) e. _V )
371 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` R ) e. _V )
372 370 371 ifcld 
 |-  ( ( ph /\ g e. D ) -> if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
373 363 369 356 372 fvmptd4 
 |-  ( ( ph /\ g e. D ) -> ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) = if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
374 55 337 251 345 368 ringrzd 
 |-  ( ( ph /\ g e. D ) -> ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) = ( 0g ` ( ( I \ J ) mPoly R ) ) )
375 8 258 286 251 23 253 mpl0 
 |-  ( ph -> ( 0g ` ( ( I \ J ) mPoly R ) ) = ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) )
376 375 adantr 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` ( ( I \ J ) mPoly R ) ) = ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) )
377 374 376 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) = ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) )
378 377 fveq1d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) = ( ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( Y |` ( I \ J ) ) ) )
379 fvex 
 |-  ( 0g ` R ) e. _V
380 379 fvconst2 
 |-  ( ( Y |` ( I \ J ) ) e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } -> ( ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( Y |` ( I \ J ) ) ) = ( 0g ` R ) )
381 356 380 syl 
 |-  ( ( ph /\ g e. D ) -> ( ( { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( Y |` ( I \ J ) ) ) = ( 0g ` R ) )
382 378 381 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) = ( 0g ` R ) )
383 373 382 ifeq12d 
 |-  ( ( ph /\ g e. D ) -> if ( ( Y |` J ) = ( g |` J ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 1r ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) , ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( 0g ` ( ( I \ J ) mPoly R ) ) ) ` ( Y |` ( I \ J ) ) ) ) = if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
384 361 383 eqtrid 
 |-  ( ( ph /\ g e. D ) -> ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) = if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
385 384 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) ) = ( ( F ` g ) ( .r ` R ) if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) )
386 ifan 
 |-  if ( ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) )
387 386 oveq2i 
 |-  ( ( F ` g ) ( .r ` R ) if ( ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( F ` g ) ( .r ` R ) if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) )
388 1 psrbagf 
 |-  ( Y e. D -> Y : I --> NN0 )
389 7 388 syl 
 |-  ( ph -> Y : I --> NN0 )
390 389 ffnd 
 |-  ( ph -> Y Fn I )
391 390 adantr 
 |-  ( ( ph /\ g e. D ) -> Y Fn I )
392 undif 
 |-  ( J C_ I <-> ( J u. ( I \ J ) ) = I )
393 5 392 sylib 
 |-  ( ph -> ( J u. ( I \ J ) ) = I )
394 393 adantr 
 |-  ( ( ph /\ g e. D ) -> ( J u. ( I \ J ) ) = I )
395 394 fneq2d 
 |-  ( ( ph /\ g e. D ) -> ( Y Fn ( J u. ( I \ J ) ) <-> Y Fn I ) )
396 391 395 mpbird 
 |-  ( ( ph /\ g e. D ) -> Y Fn ( J u. ( I \ J ) ) )
397 89 ffnd 
 |-  ( ( ph /\ g e. D ) -> g Fn I )
398 394 fneq2d 
 |-  ( ( ph /\ g e. D ) -> ( g Fn ( J u. ( I \ J ) ) <-> g Fn I ) )
399 397 398 mpbird 
 |-  ( ( ph /\ g e. D ) -> g Fn ( J u. ( I \ J ) ) )
400 eqfnun 
 |-  ( ( Y Fn ( J u. ( I \ J ) ) /\ g Fn ( J u. ( I \ J ) ) ) -> ( Y = g <-> ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) ) )
401 396 399 400 syl2anc 
 |-  ( ( ph /\ g e. D ) -> ( Y = g <-> ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) ) )
402 401 ifbid 
 |-  ( ( ph /\ g e. D ) -> if ( Y = g , ( 1r ` R ) , ( 0g ` R ) ) = if ( ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
403 402 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) if ( Y = g , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( F ` g ) ( .r ` R ) if ( ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
404 ovif2 
 |-  ( ( F ` g ) ( .r ` R ) if ( Y = g , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( Y = g , ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) , ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) )
405 403 404 eqtr3di 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) if ( ( ( Y |` J ) = ( g |` J ) /\ ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( Y = g , ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) , ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) ) )
406 387 405 eqtr3id 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) if ( ( Y |` J ) = ( g |` J ) , if ( ( Y |` ( I \ J ) ) = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) , ( 0g ` R ) ) ) = if ( Y = g , ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) , ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) ) )
407 385 406 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) ) = if ( Y = g , ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) , ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) ) )
408 4 adantr 
 |-  ( ( ph /\ g e. D ) -> R e. CRing )
409 8 258 286 365 177 159 161 58 408 367 mplcoe2 
 |-  ( ( ph /\ g e. D ) -> ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( ( g |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
410 simpr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> k e. ( I \ J ) )
411 410 fvresd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( g |` ( I \ J ) ) ` k ) = ( g ` k ) )
412 411 oveq1d 
 |-  ( ( ( ph /\ g e. D ) /\ k e. ( I \ J ) ) -> ( ( ( g |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) )
413 412 mpteq2dva 
 |-  ( ( ph /\ g e. D ) -> ( k e. ( I \ J ) |-> ( ( ( g |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) = ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) )
414 413 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( ( g |` ( I \ J ) ) ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) = ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
415 409 414 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) )
416 eqid 
 |-  ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) = ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) )
417 eqeq1 
 |-  ( j = ( Y |` J ) -> ( j = ( g |` J ) <-> ( Y |` J ) = ( g |` J ) ) )
418 417 ifbid 
 |-  ( j = ( Y |` J ) -> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) = if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) )
419 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 1r ` ( ( I \ J ) mPoly R ) ) e. _V )
420 fvexd 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` ( ( I \ J ) mPoly R ) ) e. _V )
421 419 420 ifcld 
 |-  ( ( ph /\ g e. D ) -> if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) e. _V )
422 416 418 328 421 fvmptd3 
 |-  ( ( ph /\ g e. D ) -> ( ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` J ) ) = if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) )
423 24 adantr 
 |-  ( ( ph /\ g e. D ) -> ( ( I \ J ) mPoly R ) e. CRing )
424 1 265 85 192 72 psrbagres 
 |-  ( ( ph /\ g e. D ) -> ( g |` J ) e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } )
425 9 265 251 364 207 17 18 49 423 424 mplcoe2 
 |-  ( ( ph /\ g e. D ) -> ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) = ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( ( g |` J ) ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) )
426 simpr 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> k e. J )
427 426 fvresd 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( g |` J ) ` k ) = ( g ` k ) )
428 427 oveq1d 
 |-  ( ( ( ph /\ g e. D ) /\ k e. J ) -> ( ( ( g |` J ) ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) = ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) )
429 428 mpteq2dva 
 |-  ( ( ph /\ g e. D ) -> ( k e. J |-> ( ( ( g |` J ) ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) = ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) )
430 429 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( ( g |` J ) ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) = ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) )
431 425 430 eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) = ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) )
432 431 fveq1d 
 |-  ( ( ph /\ g e. D ) -> ( ( j e. { x e. ( NN0 ^m J ) | ( `' x " NN ) e. Fin } |-> if ( j = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` J ) ) = ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) )
433 422 432 eqtr3d 
 |-  ( ( ph /\ g e. D ) -> if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) = ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) )
434 415 433 oveq12d 
 |-  ( ( ph /\ g e. D ) -> ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) = ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) )
435 434 fveq1d 
 |-  ( ( ph /\ g e. D ) -> ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) = ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ` ( Y |` ( I \ J ) ) ) )
436 435 oveq2d 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( ( ( i e. { y e. ( NN0 ^m ( I \ J ) ) | ( `' y " NN ) e. Fin } |-> if ( i = ( g |` ( I \ J ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) if ( ( Y |` J ) = ( g |` J ) , ( 1r ` ( ( I \ J ) mPoly R ) ) , ( 0g ` ( ( I \ J ) mPoly R ) ) ) ) ` ( Y |` ( I \ J ) ) ) ) = ( ( F ` g ) ( .r ` R ) ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ` ( Y |` ( I \ J ) ) ) ) )
437 69 355 365 366 76 ringridmd 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) = ( F ` g ) )
438 69 355 286 366 76 ringrzd 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
439 437 438 ifeq12d 
 |-  ( ( ph /\ g e. D ) -> if ( Y = g , ( ( F ` g ) ( .r ` R ) ( 1r ` R ) ) , ( ( F ` g ) ( .r ` R ) ( 0g ` R ) ) ) = if ( Y = g , ( F ` g ) , ( 0g ` R ) ) )
440 407 436 439 3eqtr3d 
 |-  ( ( ph /\ g e. D ) -> ( ( F ` g ) ( .r ` R ) ( ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .r ` ( ( I \ J ) mPoly R ) ) ( ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ` ( Y |` J ) ) ) ` ( Y |` ( I \ J ) ) ) ) = if ( Y = g , ( F ` g ) , ( 0g ` R ) ) )
441 354 357 440 3eqtrd 
 |-  ( ( ph /\ g e. D ) -> ( ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = if ( Y = g , ( F ` g ) , ( 0g ` R ) ) )
442 441 mpteq2dva 
 |-  ( ph -> ( g e. D |-> ( ( ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) ) = ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) )
443 336 442 eqtrd 
 |-  ( ph -> ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) = ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) )
444 443 oveq2d 
 |-  ( ph -> ( R gsum ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) = ( R gsum ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) ) )
445 59 ringcmnd 
 |-  ( ph -> R e. CMnd )
446 69 286 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
447 59 446 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
448 447 adantr 
 |-  ( ( ph /\ g e. D ) -> ( 0g ` R ) e. ( Base ` R ) )
449 76 448 ifcld 
 |-  ( ( ph /\ g e. D ) -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) e. ( Base ` R ) )
450 449 fmpttd 
 |-  ( ph -> ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) : D --> ( Base ` R ) )
451 eldifsnneq 
 |-  ( g e. ( D \ { Y } ) -> -. g = Y )
452 451 neqcomd 
 |-  ( g e. ( D \ { Y } ) -> -. Y = g )
453 452 iffalsed 
 |-  ( g e. ( D \ { Y } ) -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) = ( 0g ` R ) )
454 453 adantl 
 |-  ( ( ph /\ g e. ( D \ { Y } ) ) -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) = ( 0g ` R ) )
455 454 257 suppss2 
 |-  ( ph -> ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { Y } )
456 257 mptexd 
 |-  ( ph -> ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) e. _V )
457 funmpt 
 |-  Fun ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) )
458 457 a1i 
 |-  ( ph -> Fun ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) )
459 snfi 
 |-  { Y } e. Fin
460 459 a1i 
 |-  ( ph -> { Y } e. Fin )
461 460 455 ssfid 
 |-  ( ph -> ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) e. Fin )
462 456 447 458 461 isfsuppd 
 |-  ( ph -> ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )
463 69 286 445 257 450 455 462 gsumres 
 |-  ( ph -> ( R gsum ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) |` { Y } ) ) = ( R gsum ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) ) )
464 7 snssd 
 |-  ( ph -> { Y } C_ D )
465 464 resmptd 
 |-  ( ph -> ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) |` { Y } ) = ( g e. { Y } |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) )
466 465 oveq2d 
 |-  ( ph -> ( R gsum ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) |` { Y } ) ) = ( R gsum ( g e. { Y } |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) ) )
467 70 7 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. ( Base ` R ) )
468 iftrue 
 |-  ( Y = g -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) = ( F ` g ) )
469 468 eqcoms 
 |-  ( g = Y -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) = ( F ` g ) )
470 fveq2 
 |-  ( g = Y -> ( F ` g ) = ( F ` Y ) )
471 469 470 eqtrd 
 |-  ( g = Y -> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) = ( F ` Y ) )
472 69 471 gsumsn 
 |-  ( ( R e. Mnd /\ Y e. D /\ ( F ` Y ) e. ( Base ` R ) ) -> ( R gsum ( g e. { Y } |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) ) = ( F ` Y ) )
473 254 7 467 472 syl3anc 
 |-  ( ph -> ( R gsum ( g e. { Y } |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) ) = ( F ` Y ) )
474 466 473 eqtrd 
 |-  ( ph -> ( R gsum ( ( g e. D |-> if ( Y = g , ( F ` g ) , ( 0g ` R ) ) ) |` { Y } ) ) = ( F ` Y ) )
475 444 463 474 3eqtr2d 
 |-  ( ph -> ( R gsum ( ( v e. ( Base ` ( ( I \ J ) mPoly R ) ) |-> ( v ` ( Y |` ( I \ J ) ) ) ) o. ( ( w e. ( Base ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) |-> ( w ` ( Y |` J ) ) ) o. ( g e. D |-> ( ( ( algSc ` ( ( I \ J ) mPoly R ) ) ` ( F ` g ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( ( mulGrp ` ( ( I \ J ) mPoly R ) ) gsum ( k e. ( I \ J ) |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( ( I \ J ) mPoly R ) ) ) ( ( ( I \ J ) mVar R ) ` k ) ) ) ) ( .s ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ( ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) gsum ( k e. J |-> ( ( g ` k ) ( .g ` ( mulGrp ` ( J mPoly ( ( I \ J ) mPoly R ) ) ) ) ( ( J mVar ( ( I \ J ) mPoly R ) ) ` k ) ) ) ) ) ) ) ) ) ) = ( F ` Y ) )
476 250 326 475 3eqtrd 
 |-  ( ph -> ( ( ( ( ( I selectVars R ) ` J ) ` F ) ` ( Y |` J ) ) ` ( Y |` ( I \ J ) ) ) = ( F ` Y ) )