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 Mat R )
mat1.o 
|- .1. = ( 1r ` R )
mat1.z 
|- .0. = ( 0g ` R )
Assertion mat1 
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mat1.a 
 |-  A = ( N Mat R )
2 mat1.o 
 |-  .1. = ( 1r ` R )
3 mat1.z 
 |-  .0. = ( 0g ` R )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
6 eqid 
 |-  ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) )
7 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
8 4 5 2 3 6 7 mamumat1cl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) e. ( ( Base ` R ) ^m ( N X. N ) ) )
9 1 4 matbas2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
10 8 9 eleqtrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) e. ( Base ` A ) )
11 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
12 1 11 matmulr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
14 13 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( R maMul <. N , N , N >. ) x ) = ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) )
15 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> R e. Ring )
16 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> N e. Fin )
17 9 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. ( ( Base ` R ) ^m ( N X. N ) ) <-> x e. ( Base ` A ) ) )
18 17 biimpar 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> x e. ( ( Base ` R ) ^m ( N X. N ) ) )
19 4 15 2 3 6 16 16 11 18 mamulid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( R maMul <. N , N , N >. ) x ) = x )
20 14 19 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) = x )
21 13 oveqd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( x ( R maMul <. N , N , N >. ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) )
22 4 15 2 3 6 16 16 11 18 mamurid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( x ( R maMul <. N , N , N >. ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x )
23 21 22 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x )
24 20 23 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( Base ` A ) ) -> ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) = x /\ ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x ) )
25 24 ralrimiva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. ( Base ` A ) ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) = x /\ ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x ) )
26 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
27 eqid 
 |-  ( Base ` A ) = ( Base ` A )
28 eqid 
 |-  ( .r ` A ) = ( .r ` A )
29 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
30 27 28 29 isringid 
 |-  ( A e. Ring -> ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) e. ( Base ` A ) /\ A. x e. ( Base ` A ) ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) = x /\ ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x ) ) <-> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) )
31 26 30 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) e. ( Base ` A ) /\ A. x e. ( Base ` A ) ( ( ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ( .r ` A ) x ) = x /\ ( x ( .r ` A ) ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) = x ) ) <-> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) ) )
32 10 25 31 mpbi2and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )