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 = ( Base ` R )
	mamumat1cl.r	|- ( ph -> R e. Ring )
	mamumat1cl.o	|- .1. = ( 1r ` R )
	mamumat1cl.z	|- .0. = ( 0g ` R )
	mamumat1cl.i	|- I = ( i e. M , j e. M |-> if ( i = j , .1. , .0. ) )
	mamumat1cl.m	|- ( ph -> M e. Fin )
Assertion	mamumat1cl	|- ( ph -> I e. ( B ^m ( M X. M ) ) )

Proof

Step	Hyp	Ref	Expression
1		mamumat1cl.b	|- B = ( Base ` R )
2		mamumat1cl.r	|- ( ph -> R e. Ring )
3		mamumat1cl.o	|- .1. = ( 1r ` R )
4		mamumat1cl.z	|- .0. = ( 0g ` R )
5		mamumat1cl.i	|- I = ( i e. M , j e. M |-> if ( i = j , .1. , .0. ) )
6		mamumat1cl.m	|- ( ph -> M e. Fin )
7	1 3	ringidcl	|- ( R e. Ring -> .1. e. B )
8	1 4	ring0cl	|- ( R e. Ring -> .0. e. B )
9	7 8	ifcld	|- ( R e. Ring -> if ( i = j , .1. , .0. ) e. B )
10	2 9	syl	|- ( ph -> if ( i = j , .1. , .0. ) e. B )
11	10	adantr	|- ( ( ph /\ ( i e. M /\ j e. M ) ) -> if ( i = j , .1. , .0. ) e. B )
12	11	ralrimivva	|- ( ph -> A. i e. M A. j e. M if ( i = j , .1. , .0. ) e. B )
13	5	fmpo	|- ( A. i e. M A. j e. M if ( i = j , .1. , .0. ) e. B <-> I : ( M X. M ) --> B )
14	12 13	sylib	|- ( ph -> I : ( M X. M ) --> B )
15	1	fvexi	|- B e. _V
16		xpfi	|- ( ( M e. Fin /\ M e. Fin ) -> ( M X. M ) e. Fin )
17	6 6 16	syl2anc	|- ( ph -> ( M X. M ) e. Fin )
18		elmapg	|- ( ( B e. _V /\ ( M X. M ) e. Fin ) -> ( I e. ( B ^m ( M X. M ) ) <-> I : ( M X. M ) --> B ) )
19	15 17 18	sylancr	|- ( ph -> ( I e. ( B ^m ( M X. M ) ) <-> I : ( M X. M ) --> B ) )
20	14 19	mpbird	|- ( ph -> I e. ( B ^m ( M X. M ) ) )