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

Proof

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