# Metamath Proof Explorer

## Theorem mat1

Description: Value of an identity matrix, see also the statement in Lang p. 504: "The unit element of the ring of n x n matrices is the matrix I_n ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015)

Ref Expression
Hypotheses mat1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mat1.o
mat1.z
Assertion mat1

### Proof

Step Hyp Ref Expression
1 mat1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mat1.o
3 mat1.z
4 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
5 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
6 eqid
7 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\in \mathrm{Fin}$
8 4 5 2 3 6 7 mamumat1cl
9 1 4 matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
10 8 9 eleqtrd
11 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
12 1 11 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
13 12 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{A}}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
14 13 oveqd
15 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{A}}\right)\to {R}\in \mathrm{Ring}$
16 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{A}}\right)\to {N}\in \mathrm{Fin}$
17 9 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)↔{x}\in {\mathrm{Base}}_{{A}}\right)$
18 17 biimpar ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {\mathrm{Base}}_{{A}}\right)\to {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
19 4 15 2 3 6 16 16 11 18 mamulid
20 14 19 eqtr3d
21 13 oveqd
22 4 15 2 3 6 16 16 11 18 mamurid
23 21 22 eqtr3d
24 20 23 jca
25 24 ralrimiva
26 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
27 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
28 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
29 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
30 27 28 29 isringid
31 26 30 syl
32 10 25 31 mpbi2and