# Metamath Proof Explorer

## Theorem matsc

Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses matsc.a $⊢ A = N Mat R$
matsc.k $⊢ K = Base R$
matsc.m
matsc.z
Assertion matsc

### Proof

Step Hyp Ref Expression
1 matsc.a $⊢ A = N Mat R$
2 matsc.k $⊢ K = Base R$
3 matsc.m
4 matsc.z
5 simp3 $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ∈ K$
6 3simpa $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N ∈ Fin ∧ R ∈ Ring$
7 1 matring $⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring$
8 eqid $⊢ Base A = Base A$
9 eqid $⊢ 1 A = 1 A$
10 8 9 ringidcl $⊢ A ∈ Ring → 1 A ∈ Base A$
11 6 7 10 3syl $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → 1 A ∈ Base A$
12 eqid $⊢ ⋅ R = ⋅ R$
13 eqid $⊢ N × N = N × N$
14 1 8 2 3 12 13 matvsca2
15 5 11 14 syl2anc
16 simp1 $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N ∈ Fin$
17 simp13 $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K ∧ i ∈ N ∧ j ∈ N → L ∈ K$
18 fvex $⊢ 1 R ∈ V$
19 4 fvexi
20 18 19 ifex
21 20 a1i
22 fconstmpo $⊢ N × N × L = i ∈ N , j ∈ N ⟼ L$
23 22 a1i $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → N × N × L = i ∈ N , j ∈ N ⟼ L$
24 eqid $⊢ 1 R = 1 R$
25 1 24 4 mat1
29 2 12 24 ringridm $⊢ R ∈ Ring ∧ L ∈ K → L ⋅ R 1 R = L$
30 29 3adant1 $⊢ N ∈ Fin ∧ R ∈ Ring ∧ L ∈ K → L ⋅ R 1 R = L$