Metamath Proof Explorer

Theorem dmatmul

Description: The product of two diagonal matrices. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatmul ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) )

Proof

Step Hyp Ref Expression
1 dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
6 1 5 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
7 6 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
8 7 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( .r ‘ 𝐴 ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
9 8 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑅 ∈ Ring )
13 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑁 ∈ Fin )
14 1 2 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 → 𝑋 ∈ 𝐵 ) )
15 14 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ 𝐵 )
16 1 10 2 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17 15 16 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
18 17 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
19 1 2 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝐷 → 𝑌 ∈ 𝐵 ) )
20 19 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐷 ) → 𝑌 ∈ 𝐵 )
21 1 10 2 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
22 20 21 syl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐷 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
23 22 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
24 5 10 11 12 13 13 13 18 23 mamuval ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) ) )
25 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
26 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
27 26 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑅 ∈ CMnd )
28 27 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
29 28 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑅 ∈ CMnd )
30 13 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑁 ∈ Fin )
31 30 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
32 eqid ⊢ ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) )
33 ovexd ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ∈ V )
34 fvexd ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
35 32 31 33 34 fsuppmptdm ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
36 12 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ Ring )
37 36 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
38 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
39 38 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
40 simpr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
41 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
42 1 41 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 → 𝑋 ∈ ( Base ‘ 𝐴 ) ) )
43 42 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
44 43 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
45 44 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
46 45 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
47 1 10 matecl ⊢ ( ( 𝑥 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 𝑋 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
48 39 40 46 47 syl3anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑥 𝑋 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
49 simplr3 ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
50 1 41 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝐷 → 𝑌 ∈ ( Base ‘ 𝐴 ) ) )
51 50 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐷 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
52 51 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
53 52 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
54 53 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
55 1 10 matecl ⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑌 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
56 40 49 54 55 syl3anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
57 10 11 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 𝑋 𝑘 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
58 37 48 56 57 syl3anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
59 38 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
60 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
61 15 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ 𝐵 )
62 61 2 eleqtrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
63 62 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
64 1 10 matecl ⊢ ( ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 𝑋 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
65 38 60 63 64 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑋 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
66 50 a1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ 𝐷 → 𝑌 ∈ ( Base ‘ 𝐴 ) ) ) )
67 66 imp32 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
68 67 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
69 1 10 matecl ⊢ ( ( 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑌 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
70 38 60 68 69 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
71 10 11 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 𝑋 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
72 36 65 70 71 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
73 72 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
74 eqtr ⊢ ( ( 𝑘 = 𝑥 ∧ 𝑥 = 𝑦 ) → 𝑘 = 𝑦 )
75 74 ancoms ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑘 = 𝑥 ) → 𝑘 = 𝑦 )
76 75 oveq2d ⊢ ( ( 𝑥 = 𝑦 ∧ 𝑘 = 𝑥 ) → ( 𝑥 𝑋 𝑘 ) = ( 𝑥 𝑋 𝑦 ) )
77 76 adantlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 = 𝑥 ) → ( 𝑥 𝑋 𝑘 ) = ( 𝑥 𝑋 𝑦 ) )
78 oveq1 ⊢ ( 𝑘 = 𝑥 → ( 𝑘 𝑌 𝑦 ) = ( 𝑥 𝑌 𝑦 ) )
79 78 adantl ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 = 𝑥 ) → ( 𝑘 𝑌 𝑦 ) = ( 𝑥 𝑌 𝑦 ) )
80 77 79 oveq12d ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 = 𝑥 ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
81 10 25 29 31 35 58 59 73 80 gsumdifsnd ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ) )
82 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ 𝐷 )
83 13 12 82 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) )
84 83 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) )
85 84 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) )
86 38 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝑁 )
87 eldifi ⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) → 𝑘 ∈ 𝑁 )
88 87 adantl ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑘 ∈ 𝑁 )
89 eldifsni ⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) → 𝑘 ≠ 𝑥 )
90 89 necomd ⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) → 𝑥 ≠ 𝑘 )
91 90 adantl ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑥 ≠ 𝑘 )
92 1 2 3 4 dmatelnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑁 ∧ 𝑘 ∈ 𝑁 ∧ 𝑥 ≠ 𝑘 ) ) → ( 𝑥 𝑋 𝑘 ) = 0 )
93 85 86 88 91 92 syl13anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( 𝑥 𝑋 𝑘 ) = 0 )
94 93 oveq1d ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) )
95 36 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑅 ∈ Ring )
96 simplr3 ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑦 ∈ 𝑁 )
97 53 ad2antlr ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
98 88 96 97 55 syl3anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
99 10 11 3 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
100 95 98 99 syl2anc ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
101 94 100 eqtrd ⊢ ( ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
102 101 mpteq2dva ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) = ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ 0 ) )
103 102 oveq2d ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ 0 ) ) )
104 diffi ⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝑥 } ) ∈ Fin )
105 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
106 104 105 anim12ci ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Mnd ∧ ( 𝑁 ∖ { 𝑥 } ) ∈ Fin ) )
107 106 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑅 ∈ Mnd ∧ ( 𝑁 ∖ { 𝑥 } ) ∈ Fin ) )
108 107 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 ∈ Mnd ∧ ( 𝑁 ∖ { 𝑥 } ) ∈ Fin ) )
109 108 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 ∈ Mnd ∧ ( 𝑁 ∖ { 𝑥 } ) ∈ Fin ) )
110 3 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑁 ∖ { 𝑥 } ) ∈ Fin ) → ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ 0 ) ) = 0 )
111 109 110 syl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ 0 ) ) = 0 )
112 103 111 eqtrd ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = 0 )
113 112 oveq1d ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( ( 𝑅 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝑥 } ) ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) ( +g ‘ 𝑅 ) ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ) = ( 0 ( +g ‘ 𝑅 ) ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ) )
114 105 ad2antlr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑅 ∈ Mnd )
115 114 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ Mnd )
116 38 60 53 69 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
117 36 65 116 71 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
118 115 117 jca ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 ∈ Mnd ∧ ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) )
119 118 adantl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 ∈ Mnd ∧ ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) )
120 10 25 3 mndlid ⊢ ( ( 𝑅 ∈ Mnd ∧ ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
121 119 120 syl ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 0 ( +g ‘ 𝑅 ) ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
122 81 113 121 3eqtrd ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
123 iftrue ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
124 123 adantr ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) = ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) )
125 122 124 eqtr4d ⊢ ( ( 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) )
126 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑌 ∈ 𝐷 )
127 13 12 126 3jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷 ) )
128 127 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷 ) )
129 128 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷 ) )
130 129 adantl ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷 ) )
131 simprr ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ 𝑁 )
132 simplr3 ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
133 132 adantl ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑦 ∈ 𝑁 )
134 df-ne ⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
135 neeq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ≠ 𝑦 ↔ 𝑘 ≠ 𝑦 ) )
136 135 biimpcd ⊢ ( 𝑥 ≠ 𝑦 → ( 𝑥 = 𝑘 → 𝑘 ≠ 𝑦 ) )
137 134 136 sylbir ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑥 = 𝑘 → 𝑘 ≠ 𝑦 ) )
138 137 adantr ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑥 = 𝑘 → 𝑘 ≠ 𝑦 ) )
139 138 adantr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑥 = 𝑘 → 𝑘 ≠ 𝑦 ) )
140 139 impcom ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ≠ 𝑦 )
141 1 2 3 4 dmatelnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐷 ) ∧ ( 𝑘 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑘 ≠ 𝑦 ) ) → ( 𝑘 𝑌 𝑦 ) = 0 )
142 130 131 133 140 141 syl13anc ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑘 𝑌 𝑦 ) = 0 )
143 142 oveq2d ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) 0 ) )
144 36 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑅 ∈ Ring )
145 38 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
146 simpr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
147 63 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
148 145 146 147 47 syl3anc ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑥 𝑋 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
149 10 11 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 𝑋 𝑘 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
150 144 148 149 syl2anc ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
151 150 adantl ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) 0 ) = 0 )
152 143 151 eqtrd ⊢ ( ( 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
153 84 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) )
154 153 adantl ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐷 ) )
155 145 adantl ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑥 ∈ 𝑁 )
156 simprr ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑘 ∈ 𝑁 )
157 neqne ⊢ ( ¬ 𝑥 = 𝑘 → 𝑥 ≠ 𝑘 )
158 157 adantr ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → 𝑥 ≠ 𝑘 )
159 154 155 156 158 92 syl13anc ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 𝑥 𝑋 𝑘 ) = 0 )
160 159 oveq1d ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) )
161 68 ad2antlr ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
162 146 132 161 55 syl3anc ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑘 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
163 144 162 99 syl2anc ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
164 163 adantl ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( 0 ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
165 160 164 eqtrd ⊢ ( ( ¬ 𝑥 = 𝑘 ∧ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
166 152 165 pm2.61ian ⊢ ( ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) = 0 )
167 166 mpteq2dva ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ 0 ) )
168 167 oveq2d ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) )
169 105 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Mnd ) )
170 169 ancomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Mnd ∧ 𝑁 ∈ Fin ) )
171 3 gsumz ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑁 ∈ Fin ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) = 0 )
172 170 171 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) = 0 )
173 172 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) = 0 )
174 173 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) = 0 )
175 174 adantl ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ 0 ) ) = 0 )
176 iffalse ⊢ ( ¬ 𝑥 = 𝑦 → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) = 0 )
177 176 eqcomd ⊢ ( ¬ 𝑥 = 𝑦 → 0 = if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) )
178 177 adantr ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → 0 = if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) )
179 168 175 178 3eqtrd ⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) )
180 125 179 pm2.61ian ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) = if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) )
181 180 mpoeq3dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑥 𝑋 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑌 𝑦 ) ) ) ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) )
182 9 24 181 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) )