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𝐴 ) 𝑌 ) ∈ 𝐷 )