Metamath Proof Explorer

Theorem mamumat1cl

Description: The identity matrix (as operation in maps-to notation) is a matrix. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamumat1cl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
mamumat1cl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
mamumat1cl.o
mamumat1cl.z
mamumat1cl.i
mamumat1cl.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
Assertion mamumat1cl ${⊢}{\phi }\to {I}\in \left({{B}}^{\left({M}×{M}\right)}\right)$

Proof

Step Hyp Ref Expression
1 mamumat1cl.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 mamumat1cl.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
3 mamumat1cl.o
4 mamumat1cl.z
5 mamumat1cl.i
6 mamumat1cl.m ${⊢}{\phi }\to {M}\in \mathrm{Fin}$
7 1 3 ringidcl
8 1 4 ring0cl
9 7 8 ifcld
10 2 9 syl
14 12 13 sylib ${⊢}{\phi }\to {I}:{M}×{M}⟶{B}$
15 1 fvexi ${⊢}{B}\in \mathrm{V}$
16 xpfi ${⊢}\left({M}\in \mathrm{Fin}\wedge {M}\in \mathrm{Fin}\right)\to {M}×{M}\in \mathrm{Fin}$
17 6 6 16 syl2anc ${⊢}{\phi }\to {M}×{M}\in \mathrm{Fin}$
18 elmapg ${⊢}\left({B}\in \mathrm{V}\wedge {M}×{M}\in \mathrm{Fin}\right)\to \left({I}\in \left({{B}}^{\left({M}×{M}\right)}\right)↔{I}:{M}×{M}⟶{B}\right)$
19 15 17 18 sylancr ${⊢}{\phi }\to \left({I}\in \left({{B}}^{\left({M}×{M}\right)}\right)↔{I}:{M}×{M}⟶{B}\right)$
20 14 19 mpbird ${⊢}{\phi }\to {I}\in \left({{B}}^{\left({M}×{M}\right)}\right)$