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

Metamath Proof Explorer

Theorem mattpostpos

Description: The transpose of the transpose of a square matrix is the square matrix itself. (Contributed by SO, 17-Jul-2018)

Ref Expression
Hypotheses mattposcl.a 
|- A = ( N Mat R )
mattposcl.b 
|- B = ( Base ` A )
Assertion mattpostpos 
|- ( M e. B -> tpos tpos M = M )

Proof

Step Hyp Ref Expression
1 mattposcl.a 
 |-  A = ( N Mat R )
2 mattposcl.b 
 |-  B = ( Base ` A )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 1 3 2 matbas2i 
 |-  ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
5 elmapi 
 |-  ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
6 4 5 syl 
 |-  ( M e. B -> M : ( N X. N ) --> ( Base ` R ) )
7 frel 
 |-  ( M : ( N X. N ) --> ( Base ` R ) -> Rel M )
8 6 7 syl 
 |-  ( M e. B -> Rel M )
9 relxp 
 |-  Rel ( N X. N )
10 6 fdmd 
 |-  ( M e. B -> dom M = ( N X. N ) )
11 10 releqd 
 |-  ( M e. B -> ( Rel dom M <-> Rel ( N X. N ) ) )
12 9 11 mpbiri 
 |-  ( M e. B -> Rel dom M )
13 tpostpos2 
 |-  ( ( Rel M /\ Rel dom M ) -> tpos tpos M = M )
14 8 12 13 syl2anc 
 |-  ( M e. B -> tpos tpos M = M )