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	$$⊢\underset{\dot{}}{1}=1_R$$
	mamumat1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mamumat1cl.i	$$⊢I=\left(i\in M,j\in M⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
	mamumat1cl.m	$$⊢\phi \to M\in \mathrm{Fin}$$
Assertion	mamumat1cl	$$⊢\phi \to I\in \left(B^{\left(M\times 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	$$⊢\underset{\dot{}}{1}=1_R$$
4		mamumat1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		mamumat1cl.i	$$⊢I=\left(i\in M,j\in M⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
6		mamumat1cl.m	$$⊢\phi \to M\in \mathrm{Fin}$$
7	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
8	1 4	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
9	7 8	ifcld	$$⊢R\in \mathrm{Ring}\to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in B$$
10	2 9	syl	$$⊢\phi \to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in B$$
11	10	adantr	$$⊢\left(\phi \wedge \left(i\in M\wedge j\in M\right)\right)\to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in B$$
12	11	ralrimivva	$$⊢\phi \to \forall i\in M\forall j\in Mif\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in B$$
13	5	fmpo	$$⊢\forall i\in M\forall j\in Mif\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in B\leftrightarrow I:M\times M⟶B$$
14	12 13	sylib	$$⊢\phi \to I:M\times M⟶B$$
15	1	fvexi	$$⊢B\in \mathrm{V}$$
16		xpfi	$$⊢\left(M\in \mathrm{Fin}\wedge M\in \mathrm{Fin}\right)\to M\times M\in \mathrm{Fin}$$
17	6 6 16	syl2anc	$$⊢\phi \to M\times M\in \mathrm{Fin}$$
18		elmapg	$$⊢\left(B\in \mathrm{V}\wedge M\times M\in \mathrm{Fin}\right)\to \left(I\in \left(B^{\left(M\times M\right)}\right)\leftrightarrow I:M\times M⟶B\right)$$
19	15 17 18	sylancr	$$⊢\phi \to \left(I\in \left(B^{\left(M\times M\right)}\right)\leftrightarrow I:M\times M⟶B\right)$$
20	14 19	mpbird	$$⊢\phi \to I\in \left(B^{\left(M\times M\right)}\right)$$