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\in \left(B^{\left(I\times J\right)}\right)\to tposA\in \left(B^{\left(J\times I\right)}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elmapi	$$⊢A\in \left(B^{\left(I\times J\right)}\right)\to A:I\times J⟶B$$
2		tposf	$$⊢A:I\times J⟶B\to tposA:J\times I⟶B$$
3	1 2	syl	$$⊢A\in \left(B^{\left(I\times J\right)}\right)\to tposA:J\times I⟶B$$
4		elmapex	$$⊢A\in \left(B^{\left(I\times J\right)}\right)\to \left(B\in \mathrm{V}\wedge I\times J\in \mathrm{V}\right)$$
5		cnvxp	$$⊢{\left(I\times J\right)}^{-1}=J\times I$$
6		cnvexg	$$⊢I\times J\in \mathrm{V}\to {\left(I\times J\right)}^{-1}\in \mathrm{V}$$
7	5 6	eqeltrrid	$$⊢I\times J\in \mathrm{V}\to J\times I\in \mathrm{V}$$
8	7	anim2i	$$⊢\left(B\in \mathrm{V}\wedge I\times J\in \mathrm{V}\right)\to \left(B\in \mathrm{V}\wedge J\times I\in \mathrm{V}\right)$$
9		elmapg	$$⊢\left(B\in \mathrm{V}\wedge J\times I\in \mathrm{V}\right)\to \left(tposA\in \left(B^{\left(J\times I\right)}\right)\leftrightarrow tposA:J\times I⟶B\right)$$
10	4 8 9	3syl	$$⊢A\in \left(B^{\left(I\times J\right)}\right)\to \left(tposA\in \left(B^{\left(J\times I\right)}\right)\leftrightarrow tposA:J\times I⟶B\right)$$
11	3 10	mpbird	$$⊢A\in \left(B^{\left(I\times J\right)}\right)\to tposA\in \left(B^{\left(J\times I\right)}\right)$$