Step |
Hyp |
Ref |
Expression |
1 |
|
mattpos1.a |
|- A = ( N Mat R ) |
2 |
|
mattpos1.o |
|- .1. = ( 1r ` A ) |
3 |
|
eqid |
|- ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) |
4 |
3
|
tposmpo |
|- tpos ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) = ( j e. N , i e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) |
5 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
6 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
7 |
1 5 6
|
mat1 |
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
8 |
7
|
tposeqd |
|- ( ( N e. Fin /\ R e. Ring ) -> tpos ( 1r ` A ) = tpos ( i e. N , j e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
9 |
1 5 6
|
mat1 |
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( j e. N , i e. N |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
10 |
|
equcom |
|- ( j = i <-> i = j ) |
11 |
10
|
a1i |
|- ( ( j e. N /\ i e. N ) -> ( j = i <-> i = j ) ) |
12 |
11
|
ifbid |
|- ( ( j e. N /\ i e. N ) -> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) |
13 |
12
|
mpoeq3ia |
|- ( j e. N , i e. N |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) = ( j e. N , i e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) |
14 |
9 13
|
eqtrdi |
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( j e. N , i e. N |-> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ) ) |
15 |
4 8 14
|
3eqtr4a |
|- ( ( N e. Fin /\ R e. Ring ) -> tpos ( 1r ` A ) = ( 1r ` A ) ) |
16 |
2
|
tposeqi |
|- tpos .1. = tpos ( 1r ` A ) |
17 |
15 16 2
|
3eqtr4g |
|- ( ( N e. Fin /\ R e. Ring ) -> tpos .1. = .1. ) |