# 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}\mathrm{Mat}{R}$
matsc.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
matsc.m
matsc.z
Assertion matsc

### Proof

Step Hyp Ref Expression
1 matsc.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matsc.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 matsc.m
4 matsc.z
5 simp3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to {L}\in {K}$
6 3simpa ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
7 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
8 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
9 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
10 8 9 ringidcl ${⊢}{A}\in \mathrm{Ring}\to {1}_{{A}}\in {\mathrm{Base}}_{{A}}$
11 6 7 10 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to {1}_{{A}}\in {\mathrm{Base}}_{{A}}$
12 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
13 eqid ${⊢}{N}×{N}={N}×{N}$
14 1 8 2 3 12 13 matvsca2
15 5 11 14 syl2anc
16 simp1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to {N}\in \mathrm{Fin}$
17 simp13 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {L}\in {K}$
18 fvex ${⊢}{1}_{{R}}\in \mathrm{V}$
19 4 fvexi
20 18 19 ifex
21 20 a1i
22 fconstmpo ${⊢}\left({N}×{N}\right)×\left\{{L}\right\}=\left({i}\in {N},{j}\in {N}⟼{L}\right)$
23 22 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to \left({N}×{N}\right)×\left\{{L}\right\}=\left({i}\in {N},{j}\in {N}⟼{L}\right)$
24 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
25 1 24 4 mat1
27 16 16 17 21 23 26 offval22
28 ovif2
29 2 12 24 ringridm ${⊢}\left({R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to {L}{\cdot }_{{R}}{1}_{{R}}={L}$
30 29 3adant1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {L}\in {K}\right)\to {L}{\cdot }_{{R}}{1}_{{R}}={L}$
31 2 12 4 ringrz
33 30 32 ifeq12d
34 28 33 syl5eq
35 34 mpoeq3dv
36 15 27 35 3eqtrd