Metamath Proof Explorer

Theorem mat1ov

Description: Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018)

Ref Expression
Hypotheses mat1.a 
|- A = ( N Mat R )
mat1.o 
|- .1. = ( 1r ` R )
mat1.z 
|- .0. = ( 0g ` R )
mat1ov.n 
|- ( ph -> N e. Fin )
mat1ov.r 
|- ( ph -> R e. Ring )
mat1ov.i 
|- ( ph -> I e. N )
mat1ov.j 
|- ( ph -> J e. N )
mat1ov.u 
|- U = ( 1r ` A )
Assertion mat1ov 
|- ( ph -> ( I U J ) = 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 mat1ov.n 
 |-  ( ph -> N e. Fin )
5 mat1ov.r 
 |-  ( ph -> R e. Ring )
6 mat1ov.i 
 |-  ( ph -> I e. N )
7 mat1ov.j 
 |-  ( ph -> J e. N )
8 mat1ov.u 
 |-  U = ( 1r ` A )
9 1 2 3 mat1 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )
10 4 5 9 syl2anc 
 |-  ( ph -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )
11 8 10 syl5eq 
 |-  ( ph -> U = ( i e. N , j e. N |-> if ( i = j , .1. , .0. ) ) )
12 eqeq12 
 |-  ( ( i = I /\ j = J ) -> ( i = j <-> I = J ) )
13 12 ifbid 
 |-  ( ( i = I /\ j = J ) -> if ( i = j , .1. , .0. ) = if ( I = J , .1. , .0. ) )
14 13 adantl 
 |-  ( ( ph /\ ( i = I /\ j = J ) ) -> if ( i = j , .1. , .0. ) = if ( I = J , .1. , .0. ) )
15 2 fvexi 
 |-  .1. e. _V
16 3 fvexi 
 |-  .0. e. _V
17 15 16 ifex 
 |-  if ( I = J , .1. , .0. ) e. _V
18 17 a1i 
 |-  ( ph -> if ( I = J , .1. , .0. ) e. _V )
19 11 14 6 7 18 ovmpod 
 |-  ( ph -> ( I U J ) = if ( I = J , .1. , .0. ) )