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

Metamath Proof Explorer

Theorem mat1comp

Description: The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019)

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 mat1comp 
|- ( ( A e. M /\ J e. M ) -> ( A I J ) = if ( A = J , .1. , .0. ) )

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 eqeq1 
 |-  ( i = A -> ( i = j <-> A = j ) )
8 7 ifbid 
 |-  ( i = A -> if ( i = j , .1. , .0. ) = if ( A = j , .1. , .0. ) )
9 eqeq2 
 |-  ( j = J -> ( A = j <-> A = J ) )
10 9 ifbid 
 |-  ( j = J -> if ( A = j , .1. , .0. ) = if ( A = J , .1. , .0. ) )
11 3 fvexi 
 |-  .1. e. _V
12 4 fvexi 
 |-  .0. e. _V
13 11 12 ifex 
 |-  if ( A = J , .1. , .0. ) e. _V
14 8 10 5 13 ovmpo 
 |-  ( ( A e. M /\ J e. M ) -> ( A I J ) = if ( A = J , .1. , .0. ) )