Metamath Proof Explorer

Theorem scmatlss

Description: The set of scalar matrices is a linear subspace of the matrix algebra. (Contributed by AV, 25-Dec-2019)

Ref Expression
Hypotheses scmatlss.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatlss.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion scmatlss ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( LSubSp ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 scmatlss.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 scmatlss.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
3 1 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
4 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
5 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) )
6 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 ) )
7 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 ) )
8 eqidd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( LSubSp ‘ 𝐴 ) = ( LSubSp ‘ 𝐴 ) )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
11 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
12 eqid ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
13 9 1 10 11 12 2 scmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) } )
14 ssrab2 ⊢ { 𝑚 ∈ ( Base ‘ 𝐴 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) } ⊆ ( Base ‘ 𝐴 )
15 13 14 eqsstrdi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ ( Base ‘ 𝐴 ) )
16 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17 1 10 9 16 2 scmatid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )
18 17 ne0d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ≠ ∅ )
19 9 1 2 12 smatvscl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑆 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ∈ 𝑆 )
20 19 3adantr3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ∈ 𝑆 )
21 simpr3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 )
22 20 21 jca ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) )
23 1 10 9 16 2 scmataddcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
24 22 23 syldan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑎 ( ·𝑠 ‘ 𝐴 ) 𝑥 ) ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
25 3 4 5 6 7 8 15 18 24 islssd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( LSubSp ‘ 𝐴 ) )