Metamath Proof Explorer

Theorem scmatdmat

Description: A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
scmatdmat.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion scmatdmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
4 scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6 scmatdmat.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
7 id ⊢ ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) )
8 ifnefalse ⊢ ( 𝑖 ≠ 𝑗 → if ( 𝑖 = 𝑗 , 𝑐 , 0 ) = 0 )
9 7 8 sylan9eq ⊢ ( ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝑖 𝑚 𝑗 ) = 0 )
10 9 ex ⊢ ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) )
11 10 a1i ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
12 11 ralimdva ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) ∧ 𝑖 ∈ 𝑁 ) → ( ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
13 12 ralimdva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐸 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
14 13 rexlimdva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
15 14 ss2rabdv ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ⊆ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
16 15 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ⊆ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
17 1 2 5 3 4 scmatmats ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } )
18 1 2 4 6 dmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐷 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
19 17 18 sseq12d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ⊆ 𝐷 ↔ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ⊆ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
20 19 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → ( 𝑆 ⊆ 𝐷 ↔ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐸 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } ⊆ { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
21 16 20 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → 𝑆 ⊆ 𝐷 )
22 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝑆 )
23 21 22 sseldd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ 𝑆 ) → 𝑀 ∈ 𝐷 )
24 23 ex ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑀 ∈ 𝑆 → 𝑀 ∈ 𝐷 ) )