Metamath Proof Explorer

Theorem evlslem2

Description: A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 11-Apr-2024)

Ref Expression
Hypotheses evlslem2.p 
|- P = ( I mPoly R )
evlslem2.b 
|- B = ( Base ` P )
evlslem2.m 
|- .x. = ( .r ` S )
evlslem2.z 
|- .0. = ( 0g ` R )
evlslem2.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
evlslem2.i 
|- ( ph -> I e. W )
evlslem2.r 
|- ( ph -> R e. CRing )
evlslem2.s 
|- ( ph -> S e. CRing )
evlslem2.e1 
|- ( ph -> E e. ( P GrpHom S ) )
evlslem2.e2 
|- ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( j e. D /\ i e. D ) ) ) -> ( E ` ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j ) ( .r ` R ) ( y ` i ) ) , .0. ) ) ) = ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
Assertion evlslem2 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) )

Proof

Step Hyp Ref Expression
1 evlslem2.p 
 |-  P = ( I mPoly R )
2 evlslem2.b 
 |-  B = ( Base ` P )
3 evlslem2.m 
 |-  .x. = ( .r ` S )
4 evlslem2.z 
 |-  .0. = ( 0g ` R )
5 evlslem2.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
6 evlslem2.i 
 |-  ( ph -> I e. W )
7 evlslem2.r 
 |-  ( ph -> R e. CRing )
8 evlslem2.s 
 |-  ( ph -> S e. CRing )
9 evlslem2.e1 
 |-  ( ph -> E e. ( P GrpHom S ) )
10 evlslem2.e2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( j e. D /\ i e. D ) ) ) -> ( E ` ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j ) ( .r ` R ) ( y ` i ) ) , .0. ) ) ) = ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
11 eqid 
 |-  ( .r ` P ) = ( .r ` P )
12 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
13 ovex 
 |-  ( NN0 ^m I ) e. _V
14 5 13 rabex2 
 |-  D e. _V
15 14 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> D e. _V )
16 crngring 
 |-  ( R e. CRing -> R e. Ring )
17 7 16 syl 
 |-  ( ph -> R e. Ring )
18 1 6 17 mplringd 
 |-  ( ph -> P e. Ring )
19 18 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. Ring )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> I e. W )
22 17 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> R e. Ring )
23 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
24 1 20 2 5 23 mplelf 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x : D --> ( Base ` R ) )
25 24 ffvelcdmda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> ( x ` j ) e. ( Base ` R ) )
26 simpr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> j e. D )
27 1 5 4 20 21 22 2 25 26 mplmon2cl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. B )
28 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> I e. W )
29 17 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> R e. Ring )
30 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
31 1 20 2 5 30 mplelf 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y : D --> ( Base ` R ) )
32 31 ffvelcdmda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> ( y ` i ) e. ( Base ` R ) )
33 simpr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> i e. D )
34 1 5 4 20 28 29 2 32 33 mplmon2cl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. B )
35 14 mptex 
 |-  ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) e. _V
36 funmpt 
 |-  Fun ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) )
37 fvex 
 |-  ( 0g ` P ) e. _V
38 35 36 37 3pm3.2i 
 |-  ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) e. _V /\ Fun ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) /\ ( 0g ` P ) e. _V )
39 38 a1i 
 |-  ( ( ph /\ y e. B ) -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) e. _V /\ Fun ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) /\ ( 0g ` P ) e. _V ) )
40 simpr 
 |-  ( ( ph /\ y e. B ) -> y e. B )
41 1 2 4 40 mplelsfi 
 |-  ( ( ph /\ y e. B ) -> y finSupp .0. )
42 41 fsuppimpd 
 |-  ( ( ph /\ y e. B ) -> ( y supp .0. ) e. Fin )
43 1 20 2 5 40 mplelf 
 |-  ( ( ph /\ y e. B ) -> y : D --> ( Base ` R ) )
44 ssidd 
 |-  ( ( ph /\ y e. B ) -> ( y supp .0. ) C_ ( y supp .0. ) )
45 14 a1i 
 |-  ( ( ph /\ y e. B ) -> D e. _V )
46 4 fvexi 
 |-  .0. e. _V
47 46 a1i 
 |-  ( ( ph /\ y e. B ) -> .0. e. _V )
48 43 44 45 47 suppssr 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( y ` j ) = .0. )
49 48 ifeq1d 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> if ( k = j , ( y ` j ) , .0. ) = if ( k = j , .0. , .0. ) )
50 ifid 
 |-  if ( k = j , .0. , .0. ) = .0.
51 49 50 eqtrdi 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> if ( k = j , ( y ` j ) , .0. ) = .0. )
52 51 mpteq2dv 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( k e. D |-> .0. ) )
53 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
54 17 53 syl 
 |-  ( ph -> R e. Grp )
55 1 5 4 12 6 54 mpl0 
 |-  ( ph -> ( 0g ` P ) = ( D X. { .0. } ) )
56 fconstmpt 
 |-  ( D X. { .0. } ) = ( k e. D |-> .0. )
57 55 56 eqtrdi 
 |-  ( ph -> ( 0g ` P ) = ( k e. D |-> .0. ) )
58 57 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( 0g ` P ) = ( k e. D |-> .0. ) )
59 52 58 eqtr4d 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( 0g ` P ) )
60 59 45 suppss2 
 |-  ( ( ph /\ y e. B ) -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) supp ( 0g ` P ) ) C_ ( y supp .0. ) )
61 suppssfifsupp 
 |-  ( ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) e. _V /\ Fun ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( y supp .0. ) e. Fin /\ ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) supp ( 0g ` P ) ) C_ ( y supp .0. ) ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
62 39 42 60 61 syl12anc 
 |-  ( ( ph /\ y e. B ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
63 62 ralrimiva 
 |-  ( ph -> A. y e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
64 fveq1 
 |-  ( y = x -> ( y ` j ) = ( x ` j ) )
65 64 ifeq1d 
 |-  ( y = x -> if ( k = j , ( y ` j ) , .0. ) = if ( k = j , ( x ` j ) , .0. ) )
66 65 mpteq2dv 
 |-  ( y = x -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) )
67 66 mpteq2dv 
 |-  ( y = x -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) = ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
68 67 breq1d 
 |-  ( y = x -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) <-> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) ) )
69 68 cbvralvw 
 |-  ( A. y e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) <-> A. x e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
70 63 69 sylib 
 |-  ( ph -> A. x e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
71 70 r19.21bi 
 |-  ( ( ph /\ x e. B ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
72 71 adantrr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
73 equequ2 
 |-  ( i = j -> ( k = i <-> k = j ) )
74 fveq2 
 |-  ( i = j -> ( y ` i ) = ( y ` j ) )
75 73 74 ifbieq1d 
 |-  ( i = j -> if ( k = i , ( y ` i ) , .0. ) = if ( k = j , ( y ` j ) , .0. ) )
76 75 mpteq2dv 
 |-  ( i = j -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) = ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) )
77 76 cbvmptv 
 |-  ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) = ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) )
78 62 adantrl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
79 77 78 eqbrtrid 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) finSupp ( 0g ` P ) )
80 2 11 12 15 15 19 27 34 72 79 gsumdixp 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ( .r ` P ) ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) = ( P gsum ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
81 80 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ( .r ` P ) ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( E ` ( P gsum ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
82 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
83 18 82 syl 
 |-  ( ph -> P e. CMnd )
84 83 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. CMnd )
85 crngring 
 |-  ( S e. CRing -> S e. Ring )
86 8 85 syl 
 |-  ( ph -> S e. Ring )
87 86 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. Ring )
88 ringmnd 
 |-  ( S e. Ring -> S e. Mnd )
89 87 88 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. Mnd )
90 14 14 xpex 
 |-  ( D X. D ) e. _V
91 90 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( D X. D ) e. _V )
92 ghmmhm 
 |-  ( E e. ( P GrpHom S ) -> E e. ( P MndHom S ) )
93 9 92 syl 
 |-  ( ph -> E e. ( P MndHom S ) )
94 93 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E e. ( P MndHom S ) )
95 18 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> P e. Ring )
96 27 adantrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. B )
97 34 adantrl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. B )
98 2 11 ringcl 
 |-  ( ( P e. Ring /\ ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. B /\ ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. B ) -> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) e. B )
99 95 96 97 98 syl3anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) e. B )
100 99 ralrimivva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A. j e. D A. i e. D ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) e. B )
101 eqid 
 |-  ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
102 101 fmpo 
 |-  ( A. j e. D A. i e. D ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) e. B <-> ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) : ( D X. D ) --> B )
103 100 102 sylib 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) : ( D X. D ) --> B )
104 14 14 mpoex 
 |-  ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V
105 101 mpofun 
 |-  Fun ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
106 104 105 37 3pm3.2i 
 |-  ( ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` P ) e. _V )
107 106 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` P ) e. _V ) )
108 72 fsuppimpd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin )
109 79 fsuppimpd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin )
110 xpfi 
 |-  ( ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin /\ ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin ) -> ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) X. ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) e. Fin )
111 108 109 110 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) X. ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) e. Fin )
112 2 12 11 19 27 34 15 15 evlslem4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) supp ( 0g ` P ) ) C_ ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) X. ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) )
113 suppssfifsupp 
 |-  ( ( ( ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` P ) e. _V ) /\ ( ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) X. ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) e. Fin /\ ( ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) supp ( 0g ` P ) ) C_ ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) X. ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) ) ) -> ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) finSupp ( 0g ` P ) )
114 107 111 112 113 syl12anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) finSupp ( 0g ` P ) )
115 2 12 84 89 91 94 103 114 gsummhm 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( E ` ( P gsum ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
116 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> I e. W )
117 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> R e. CRing )
118 eqid 
 |-  ( .r ` R ) = ( .r ` R )
119 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> j e. D )
120 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> i e. D )
121 25 adantrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( x ` j ) e. ( Base ` R ) )
122 32 adantrl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( y ` i ) e. ( Base ` R ) )
123 1 5 4 20 116 117 11 118 119 120 121 122 mplmon2mul 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) = ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j ) ( .r ` R ) ( y ` i ) ) , .0. ) ) )
124 123 fveq2d 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( E ` ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j ) ( .r ` R ) ( y ` i ) ) , .0. ) ) ) )
125 10 anassrs 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( E ` ( k e. D |-> if ( k = ( j oF + i ) , ( ( x ` j ) ( .r ` R ) ( y ` i ) ) , .0. ) ) ) = ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
126 124 125 eqtrd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
127 126 3impb 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D /\ i e. D ) -> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
128 127 mpoeq3dva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D , i e. D |-> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) = ( j e. D , i e. D |-> ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
129 128 oveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( j e. D , i e. D |-> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( S gsum ( j e. D , i e. D |-> ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
130 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
131 eqid 
 |-  ( Base ` S ) = ( Base ` S )
132 2 131 ghmf 
 |-  ( E e. ( P GrpHom S ) -> E : B --> ( Base ` S ) )
133 9 132 syl 
 |-  ( ph -> E : B --> ( Base ` S ) )
134 133 feqmptd 
 |-  ( ph -> E = ( z e. B |-> ( E ` z ) ) )
135 134 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E = ( z e. B |-> ( E ` z ) ) )
136 fveq2 
 |-  ( z = ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) -> ( E ` z ) = ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
137 99 130 135 136 fmpoco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E o. ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) = ( j e. D , i e. D |-> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
138 137 oveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( S gsum ( j e. D , i e. D |-> ( E ` ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
139 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) = ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
140 fveq2 
 |-  ( z = ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) -> ( E ` z ) = ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
141 27 139 135 140 fmptco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) = ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) )
142 141 oveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) = ( S gsum ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) )
143 eqidd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) = ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
144 fveq2 
 |-  ( z = ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) -> ( E ` z ) = ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
145 34 143 135 144 fmptco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) = ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
146 145 oveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) = ( S gsum ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
147 142 146 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( ( S gsum ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
148 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
149 133 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> E : B --> ( Base ` S ) )
150 149 27 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) e. ( Base ` S ) )
151 133 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> E : B --> ( Base ` S ) )
152 151 34 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) e. ( Base ` S ) )
153 14 mptex 
 |-  ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) e. _V
154 funmpt 
 |-  Fun ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
155 fvex 
 |-  ( 0g ` S ) e. _V
156 153 154 155 3pm3.2i 
 |-  ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V )
157 156 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V ) )
158 ssidd 
 |-  ( ph -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) C_ ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) )
159 12 148 ghmid 
 |-  ( E e. ( P GrpHom S ) -> ( E ` ( 0g ` P ) ) = ( 0g ` S ) )
160 9 159 syl 
 |-  ( ph -> ( E ` ( 0g ` P ) ) = ( 0g ` S ) )
161 14 mptex 
 |-  ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. _V
162 161 a1i 
 |-  ( ( ph /\ j e. D ) -> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. _V )
163 37 a1i 
 |-  ( ph -> ( 0g ` P ) e. _V )
164 158 160 162 163 suppssfv 
 |-  ( ph -> ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) )
165 164 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) )
166 suppssfifsupp 
 |-  ( ( ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) e. _V /\ Fun ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V ) /\ ( ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin /\ ( ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) supp ( 0g ` P ) ) ) ) -> ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
167 157 108 165 166 syl12anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
168 14 mptex 
 |-  ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V
169 funmpt 
 |-  Fun ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
170 168 169 155 3pm3.2i 
 |-  ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V )
171 170 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V ) )
172 ssidd 
 |-  ( ph -> ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) C_ ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) )
173 14 mptex 
 |-  ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. _V
174 173 a1i 
 |-  ( ( ph /\ i e. D ) -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. _V )
175 172 160 174 163 suppssfv 
 |-  ( ph -> ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) )
176 175 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) )
177 suppssfifsupp 
 |-  ( ( ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V /\ Fun ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) /\ ( 0g ` S ) e. _V ) /\ ( ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) e. Fin /\ ( ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) supp ( 0g ` S ) ) C_ ( ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) supp ( 0g ` P ) ) ) ) -> ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
178 171 109 176 177 syl12anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
179 131 3 148 15 15 87 150 152 167 178 gsumdixp 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( S gsum ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( S gsum ( j e. D , i e. D |-> ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
180 147 179 eqtrd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( S gsum ( j e. D , i e. D |-> ( ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) .x. ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
181 129 138 180 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( j e. D , i e. D |-> ( ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ( .r ` P ) ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
182 81 115 181 3eqtr2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ( .r ` P ) ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) = ( ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
183 6 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> I e. W )
184 17 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
185 1 5 4 2 183 184 23 mplcoe4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x = ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) )
186 1 5 4 2 183 184 30 mplcoe4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y = ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
187 185 186 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` P ) y ) = ( ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ( .r ` P ) ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
188 187 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( E ` ( ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ( .r ` P ) ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
189 185 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` x ) = ( E ` ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) )
190 27 fmpttd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) : D --> B )
191 2 12 84 89 15 94 190 72 gsummhm 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) = ( E ` ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) )
192 189 191 eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` x ) = ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) )
193 186 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` y ) = ( E ` ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
194 34 fmpttd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) : D --> B )
195 2 12 84 89 15 94 194 79 gsummhm 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) = ( E ` ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
196 193 195 eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` y ) = ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) )
197 192 196 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( E ` x ) .x. ( E ` y ) ) = ( ( S gsum ( E o. ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) ) .x. ( S gsum ( E o. ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) ) ) )
198 182 188 197 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) )