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