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

Metamath Proof Explorer

Theorem tposmap

Description: The transposition of an I X J -matrix is a J X I -matrix, see also the statement in Lang p. 505. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Assertion tposmap 
|- ( A e. ( B ^m ( I X. J ) ) -> tpos A e. ( B ^m ( J X. I ) ) )

Proof

Step Hyp Ref Expression
1 elmapi 
 |-  ( A e. ( B ^m ( I X. J ) ) -> A : ( I X. J ) --> B )
2 tposf 
 |-  ( A : ( I X. J ) --> B -> tpos A : ( J X. I ) --> B )
3 1 2 syl 
 |-  ( A e. ( B ^m ( I X. J ) ) -> tpos A : ( J X. I ) --> B )
4 elmapex 
 |-  ( A e. ( B ^m ( I X. J ) ) -> ( B e. _V /\ ( I X. J ) e. _V ) )
5 cnvxp 
 |-  `' ( I X. J ) = ( J X. I )
6 cnvexg 
 |-  ( ( I X. J ) e. _V -> `' ( I X. J ) e. _V )
7 5 6 eqeltrrid 
 |-  ( ( I X. J ) e. _V -> ( J X. I ) e. _V )
8 7 anim2i 
 |-  ( ( B e. _V /\ ( I X. J ) e. _V ) -> ( B e. _V /\ ( J X. I ) e. _V ) )
9 elmapg 
 |-  ( ( B e. _V /\ ( J X. I ) e. _V ) -> ( tpos A e. ( B ^m ( J X. I ) ) <-> tpos A : ( J X. I ) --> B ) )
10 4 8 9 3syl 
 |-  ( A e. ( B ^m ( I X. J ) ) -> ( tpos A e. ( B ^m ( J X. I ) ) <-> tpos A : ( J X. I ) --> B ) )
11 3 10 mpbird 
 |-  ( A e. ( B ^m ( I X. J ) ) -> tpos A e. ( B ^m ( J X. I ) ) )