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 ABI×JtposABJ×I

Proof

Step Hyp Ref Expression
1 elmapi ABI×JA:I×JB
2 tposf A:I×JBtposA:J×IB
3 1 2 syl ABI×JtposA:J×IB
4 elmapex ABI×JBVI×JV
5 cnvxp I×J-1=J×I
6 cnvexg I×JVI×J-1V
7 5 6 eqeltrrid I×JVJ×IV
8 7 anim2i BVI×JVBVJ×IV
9 elmapg BVJ×IVtposABJ×ItposA:J×IB
10 4 8 9 3syl ABI×JtposABJ×ItposA:J×IB
11 3 10 mpbird ABI×JtposABJ×I