This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 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 ) ) )