This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐸 ‘ 𝑥 ) · ( 𝐸 ‘ 𝑦 ) ) )