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