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