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 𝑃 = ( 𝐼 mPoly 𝑅 )
evlslem2.b 𝐵 = ( Base ‘ 𝑃 )
evlslem2.m · = ( .r𝑆 )
evlslem2.z 0 = ( 0g𝑅 )
evlslem2.d 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
evlslem2.i ( 𝜑𝐼𝑊 )
evlslem2.r ( 𝜑𝑅 ∈ CRing )
evlslem2.s ( 𝜑𝑆 ∈ CRing )
evlslem2.e1 ( 𝜑𝐸 ∈ ( 𝑃 GrpHom 𝑆 ) )
evlslem2.e2 ( ( 𝜑 ∧ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑗𝐷𝑖𝐷 ) ) ) → ( 𝐸 ‘ ( 𝑘𝐷 ↦ if ( 𝑘 = ( 𝑗f + 𝑖 ) , ( ( 𝑥𝑗 ) ( .r𝑅 ) ( 𝑦𝑖 ) ) , 0 ) ) ) = ( ( 𝐸 ‘ ( 𝑘𝐷 ↦ if ( 𝑘 = 𝑗 , ( 𝑥𝑗 ) , 0 ) ) ) · ( 𝐸 ‘ ( 𝑘𝐷 ↦ if ( 𝑘 = 𝑖 , ( 𝑦𝑖 ) , 0 ) ) ) ) )
Assertion evlslem2 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐸 ‘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) = ( ( 𝐸𝑥 ) · ( 𝐸𝑦 ) ) )

Proof

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