Metamath Proof Explorer


Theorem mattpos1

Description: The transposition of the identity matrix is the identity matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses mattpos1.a
|- A = ( N Mat R )
mattpos1.o
|- .1. = ( 1r ` A )
Assertion mattpos1
|- ( ( N e. Fin /\ R e. Ring ) -> tpos .1. = .1. )

Proof

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. )