Metamath Proof Explorer

Theorem dmatmulcl

Description: The product of two diagonal matrices is a diagonal matrix. (Contributed by AV, 20-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 dmatmulcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5 oveq ⊢ ( 𝑚 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) )
6 5 eqeq1d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) → ( ( 𝑖 𝑚 𝑗 ) = 0 ↔ ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 ) )
7 6 imbi2d ⊢ ( 𝑚 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ↔ ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 ) ) )
8 7 2ralbidv ⊢ ( 𝑚 = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 ) ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑁 ∈ Fin )
11 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑅 ∈ Ring )
12 11 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑅 ∈ Ring )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑥 ∈ 𝑁 )
15 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑦 ∈ 𝑁 )
16 1 13 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋 ∈ 𝐷 → 𝑋 ∈ ( Base ‘ 𝐴 ) ) )
17 16 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋 ∈ 𝐷 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
18 17 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
19 18 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
20 1 9 13 14 15 19 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑋 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
21 1 13 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌 ∈ 𝐷 → 𝑌 ∈ ( Base ‘ 𝐴 ) ) )
22 21 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐷 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
23 22 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
24 23 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 𝑌 ∈ ( Base ‘ 𝐴 ) )
25 1 9 13 14 15 24 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
26 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
27 9 26 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 𝑋 𝑦 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑥 𝑌 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
28 12 20 25 27 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) ∈ ( Base ‘ 𝑅 ) )
29 9 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
30 29 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 0 ∈ ( Base ‘ 𝑅 ) )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
32 31 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → 0 ∈ ( Base ‘ 𝑅 ) )
33 28 32 ifcld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ) → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ∈ ( Base ‘ 𝑅 ) )
34 1 9 2 10 11 33 matbas2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) ∈ 𝐵 )
35 eqidd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) )
36 eqeq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 = 𝑦 ↔ 𝑖 = 𝑗 ) )
37 oveq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 𝑋 𝑦 ) = ( 𝑖 𝑋 𝑗 ) )
38 oveq12 ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( 𝑥 𝑌 𝑦 ) = ( 𝑖 𝑌 𝑗 ) )
39 37 38 oveq12d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) = ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
40 36 39 ifbieq1d ⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) = if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) )
41 40 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) ∧ ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) ) → if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) = if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) )
42 simplrl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ∈ 𝑁 )
43 simplrr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ∈ 𝑁 )
44 ovex ⊢ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ∈ V
45 3 fvexi ⊢ 0 ∈ V
46 44 45 ifex ⊢ if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) ∈ V
47 46 a1i ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) ∈ V )
48 35 41 42 43 47 ovmpod ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) )
49 ifnefalse ⊢ ( 𝑖 ≠ 𝑗 → if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) = 0 )
50 49 adantl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → if ( 𝑖 = 𝑗 , ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) , 0 ) = 0 )
51 48 50 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 )
52 51 ex ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 ) )
53 52 ralrimivva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) 𝑗 ) = 0 ) )
54 8 34 53 elrabd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) ∈ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
55 1 2 3 4 dmatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) = ( 𝑥 ∈ 𝑁 , 𝑦 ∈ 𝑁 ↦ if ( 𝑥 = 𝑦 , ( ( 𝑥 𝑋 𝑦 ) ( .r ‘ 𝑅 ) ( 𝑥 𝑌 𝑦 ) ) , 0 ) ) )
56 1 2 3 4 dmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐷 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
57 56 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → 𝐷 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
58 54 55 57 3eltr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ) → ( 𝑋 ( .r ‘ 𝐴 ) 𝑌 ) ∈ 𝐷 )