Metamath Proof Explorer

Theorem dmatscmcl

Description: The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019)

Ref Expression
Hypotheses dmatscmcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
dmatscmcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
dmatscmcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
dmatscmcl.s ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
dmatscmcl.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatscmcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ( 𝐶 ∗ 𝑀 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 dmatscmcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 dmatscmcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 dmatscmcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 dmatscmcl.s ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
5 dmatscmcl.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
6 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → 𝐶 ∈ 𝐾 )
7 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8 2 3 7 5 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐷 → 𝑀 ∈ 𝐵 ) )
9 8 com12 ⊢ ( 𝑀 ∈ 𝐷 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ 𝐵 ) )
10 9 adantl ⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑀 ∈ 𝐵 ) )
11 10 impcom ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → 𝑀 ∈ 𝐵 )
12 6 11 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) )
13 1 2 3 4 matvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) ) → ( 𝐶 ∗ 𝑀 ) ∈ 𝐵 )
14 12 13 syldan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ( 𝐶 ∗ 𝑀 ) ∈ 𝐵 )
15 2 3 7 5 dmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝐷 ↔ ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) ) )
16 15 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → ( 𝑀 ∈ 𝐷 ↔ ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) ) )
17 simp-4r ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
18 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → 𝐶 ∈ 𝐾 )
19 18 anim1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) )
20 19 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) )
21 simpr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
22 17 20 21 3jca ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
23 22 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
24 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
25 2 3 1 4 24 matvscacell ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 𝑖 𝑀 𝑗 ) ) )
26 23 25 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 𝑖 𝑀 𝑗 ) ) )
27 oveq2 ⊢ ( ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 𝑖 𝑀 𝑗 ) ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
28 27 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 𝑖 𝑀 𝑗 ) ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) )
29 1 24 7 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐾 ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
30 29 ad5ant23 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
31 30 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
32 26 28 31 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) )
33 32 ex ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
34 33 imim2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) )
35 34 ralimdvva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) ∧ 𝑀 ∈ 𝐵 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) )
36 35 expimpd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → ( ( 𝑀 ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑀 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) )
37 16 36 sylbid ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐶 ∈ 𝐾 ) → ( 𝑀 ∈ 𝐷 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) )
38 37 impr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) )
39 2 3 7 5 dmatel ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝐶 ∗ 𝑀 ) ∈ 𝐷 ↔ ( ( 𝐶 ∗ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) ) )
40 39 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ( ( 𝐶 ∗ 𝑀 ) ∈ 𝐷 ↔ ( ( 𝐶 ∗ 𝑀 ) ∈ 𝐵 ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 ( 𝐶 ∗ 𝑀 ) 𝑗 ) = ( 0g ‘ 𝑅 ) ) ) ) )
41 14 38 40 mpbir2and ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑀 ∈ 𝐷 ) ) → ( 𝐶 ∗ 𝑀 ) ∈ 𝐷 )