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 7 adantr 
 |-  ( ( ph /\ y e. B ) -> R e. CRing )
42 1 2 4 40 41 mplelsfi 
 |-  ( ( ph /\ y e. B ) -> y finSupp .0. )
43 42 fsuppimpd 
 |-  ( ( ph /\ y e. B ) -> ( y supp .0. ) e. Fin )
44 1 20 2 5 40 mplelf 
 |-  ( ( ph /\ y e. B ) -> y : D --> ( Base ` R ) )
45 ssidd 
 |-  ( ( ph /\ y e. B ) -> ( y supp .0. ) C_ ( y supp .0. ) )
46 14 a1i 
 |-  ( ( ph /\ y e. B ) -> D e. _V )
47 4 fvexi 
 |-  .0. e. _V
48 47 a1i 
 |-  ( ( ph /\ y e. B ) -> .0. e. _V )
49 44 45 46 48 suppssr 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( y ` j ) = .0. )
50 49 ifeq1d 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> if ( k = j , ( y ` j ) , .0. ) = if ( k = j , .0. , .0. ) )
51 ifid 
 |-  if ( k = j , .0. , .0. ) = .0.
52 50 51 eqtrdi 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> if ( k = j , ( y ` j ) , .0. ) = .0. )
53 52 mpteq2dv 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( k e. D |-> .0. ) )
54 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
55 17 54 syl 
 |-  ( ph -> R e. Grp )
56 1 5 4 12 6 55 mpl0 
 |-  ( ph -> ( 0g ` P ) = ( D X. { .0. } ) )
57 fconstmpt 
 |-  ( D X. { .0. } ) = ( k e. D |-> .0. )
58 56 57 eqtrdi 
 |-  ( ph -> ( 0g ` P ) = ( k e. D |-> .0. ) )
59 58 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( 0g ` P ) = ( k e. D |-> .0. ) )
60 53 59 eqtr4d 
 |-  ( ( ( ph /\ y e. B ) /\ j e. ( D \ ( y supp .0. ) ) ) -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( 0g ` P ) )
61 60 46 suppss2 
 |-  ( ( ph /\ y e. B ) -> ( ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) supp ( 0g ` P ) ) C_ ( y supp .0. ) )
62 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 ) )
63 39 43 61 62 syl12anc 
 |-  ( ( ph /\ y e. B ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
64 63 ralrimiva 
 |-  ( ph -> A. y e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
65 fveq1 
 |-  ( y = x -> ( y ` j ) = ( x ` j ) )
66 65 ifeq1d 
 |-  ( y = x -> if ( k = j , ( y ` j ) , .0. ) = if ( k = j , ( x ` j ) , .0. ) )
67 66 mpteq2dv 
 |-  ( y = x -> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) = ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) )
68 67 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. ) ) ) )
69 68 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 ) ) )
70 69 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 ) )
71 64 70 sylib 
 |-  ( ph -> A. x e. B ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
72 71 r19.21bi 
 |-  ( ( ph /\ x e. B ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
73 72 adantrr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
74 equequ2 
 |-  ( i = j -> ( k = i <-> k = j ) )
75 fveq2 
 |-  ( i = j -> ( y ` i ) = ( y ` j ) )
76 74 75 ifbieq1d 
 |-  ( i = j -> if ( k = i , ( y ` i ) , .0. ) = if ( k = j , ( y ` j ) , .0. ) )
77 76 mpteq2dv 
 |-  ( i = j -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) = ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) )
78 77 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. ) ) )
79 63 adantrl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( y ` j ) , .0. ) ) ) finSupp ( 0g ` P ) )
80 78 79 eqbrtrid 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) finSupp ( 0g ` P ) )
81 2 11 12 15 15 19 27 34 73 80 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. ) ) ) ) ) )
82 81 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. ) ) ) ) ) ) )
83 ringcmn 
 |-  ( P e. Ring -> P e. CMnd )
84 18 83 syl 
 |-  ( ph -> P e. CMnd )
85 84 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> P e. CMnd )
86 crngring 
 |-  ( S e. CRing -> S e. Ring )
87 8 86 syl 
 |-  ( ph -> S e. Ring )
88 87 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. Ring )
89 ringmnd 
 |-  ( S e. Ring -> S e. Mnd )
90 88 89 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. Mnd )
91 14 14 xpex 
 |-  ( D X. D ) e. _V
92 91 a1i 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( D X. D ) e. _V )
93 ghmmhm 
 |-  ( E e. ( P GrpHom S ) -> E e. ( P MndHom S ) )
94 9 93 syl 
 |-  ( ph -> E e. ( P MndHom S ) )
95 94 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E e. ( P MndHom S ) )
96 18 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> P e. Ring )
97 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 )
98 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 )
99 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 )
100 96 97 98 99 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 )
101 100 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 )
102 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. ) ) ) )
103 102 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 )
104 101 103 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 )
105 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
106 102 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. ) ) ) )
107 105 106 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 )
108 107 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 ) )
109 73 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 )
110 80 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 )
111 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 )
112 109 110 111 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 )
113 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 ) ) ) )
114 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 ) )
115 108 112 113 114 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 ) )
116 2 12 85 90 92 95 104 115 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. ) ) ) ) ) ) )
117 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> I e. W )
118 7 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> R e. CRing )
119 eqid 
 |-  ( .r ` R ) = ( .r ` R )
120 simprl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> j e. D )
121 simprr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> i e. D )
122 25 adantrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( x ` j ) e. ( Base ` R ) )
123 32 adantrl 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ ( j e. D /\ i e. D ) ) -> ( y ` i ) e. ( Base ` R ) )
124 1 5 4 20 117 118 11 119 120 121 122 123 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. ) ) )
125 124 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. ) ) ) )
126 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. ) ) ) ) )
127 125 126 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. ) ) ) ) )
128 127 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. ) ) ) ) )
129 128 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. ) ) ) ) ) )
130 129 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. ) ) ) ) ) ) )
131 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. ) ) ) ) )
132 eqid 
 |-  ( Base ` S ) = ( Base ` S )
133 2 132 ghmf 
 |-  ( E e. ( P GrpHom S ) -> E : B --> ( Base ` S ) )
134 9 133 syl 
 |-  ( ph -> E : B --> ( Base ` S ) )
135 134 feqmptd 
 |-  ( ph -> E = ( z e. B |-> ( E ` z ) ) )
136 135 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E = ( z e. B |-> ( E ` z ) ) )
137 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. ) ) ) ) )
138 100 131 136 137 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. ) ) ) ) ) )
139 138 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. ) ) ) ) ) ) )
140 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. ) ) ) )
141 fveq2 
 |-  ( z = ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) -> ( E ` z ) = ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
142 27 140 136 141 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. ) ) ) ) )
143 142 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. ) ) ) ) ) )
144 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. ) ) ) )
145 fveq2 
 |-  ( z = ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) -> ( E ` z ) = ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
146 34 144 136 145 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. ) ) ) ) )
147 146 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. ) ) ) ) ) )
148 143 147 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. ) ) ) ) ) ) )
149 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
150 134 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ j e. D ) -> E : B --> ( Base ` S ) )
151 150 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 ) )
152 134 ad2antrr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ i e. D ) -> E : B --> ( Base ` S ) )
153 152 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 ) )
154 14 mptex 
 |-  ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) e. _V
155 funmpt 
 |-  Fun ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) )
156 fvex 
 |-  ( 0g ` S ) e. _V
157 154 155 156 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 )
158 157 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 ) )
159 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 ) ) )
160 12 149 ghmid 
 |-  ( E e. ( P GrpHom S ) -> ( E ` ( 0g ` P ) ) = ( 0g ` S ) )
161 9 160 syl 
 |-  ( ph -> ( E ` ( 0g ` P ) ) = ( 0g ` S ) )
162 14 mptex 
 |-  ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. _V
163 162 a1i 
 |-  ( ( ph /\ j e. D ) -> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) e. _V )
164 37 a1i 
 |-  ( ph -> ( 0g ` P ) e. _V )
165 159 161 163 164 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 ) ) )
166 165 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 ) ) )
167 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 ) )
168 158 109 166 167 syl12anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( E ` ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
169 14 mptex 
 |-  ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) e. _V
170 funmpt 
 |-  Fun ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) )
171 169 170 156 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 )
172 171 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 ) )
173 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 ) ) )
174 14 mptex 
 |-  ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. _V
175 174 a1i 
 |-  ( ( ph /\ i e. D ) -> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) e. _V )
176 173 161 175 164 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 ) ) )
177 176 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 ) ) )
178 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 ) )
179 172 110 177 178 syl12anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( E ` ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) finSupp ( 0g ` S ) )
180 132 3 149 15 15 88 151 153 168 179 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. ) ) ) ) ) ) )
181 148 180 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. ) ) ) ) ) ) )
182 130 139 181 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. ) ) ) ) ) ) )
183 82 116 182 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. ) ) ) ) ) ) )
184 6 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> I e. W )
185 17 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
186 1 5 4 2 184 185 23 mplcoe4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x = ( P gsum ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) ) )
187 1 5 4 2 184 185 30 mplcoe4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y = ( P gsum ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) ) )
188 186 187 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. ) ) ) ) ) )
189 188 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. ) ) ) ) ) ) )
190 186 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. ) ) ) ) ) )
191 27 fmpttd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( j e. D |-> ( k e. D |-> if ( k = j , ( x ` j ) , .0. ) ) ) : D --> B )
192 2 12 85 90 15 95 191 73 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. ) ) ) ) ) )
193 190 192 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. ) ) ) ) ) )
194 187 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. ) ) ) ) ) )
195 34 fmpttd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. D |-> ( k e. D |-> if ( k = i , ( y ` i ) , .0. ) ) ) : D --> B )
196 2 12 85 90 15 95 195 80 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. ) ) ) ) ) )
197 194 196 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. ) ) ) ) ) )
198 193 197 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. ) ) ) ) ) ) )
199 183 189 198 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E ` ( x ( .r ` P ) y ) ) = ( ( E ` x ) .x. ( E ` y ) ) )