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