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