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	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elmapi	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → 𝐴 : ( 𝐼 × 𝐽 ) ⟶ 𝐵 )
2		tposf	⊢ ( 𝐴 : ( 𝐼 × 𝐽 ) ⟶ 𝐵 → tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 )
3	1 2	syl	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 )
4		elmapex	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → ( 𝐵 ∈ V ∧ ( 𝐼 × 𝐽 ) ∈ V ) )
5		cnvxp	⊢ ◡ ( 𝐼 × 𝐽 ) = ( 𝐽 × 𝐼 )
6		cnvexg	⊢ ( ( 𝐼 × 𝐽 ) ∈ V → ◡ ( 𝐼 × 𝐽 ) ∈ V )
7	5 6	eqeltrrid	⊢ ( ( 𝐼 × 𝐽 ) ∈ V → ( 𝐽 × 𝐼 ) ∈ V )
8	7	anim2i	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐼 × 𝐽 ) ∈ V ) → ( 𝐵 ∈ V ∧ ( 𝐽 × 𝐼 ) ∈ V ) )
9		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐽 × 𝐼 ) ∈ V ) → ( tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) ↔ tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) )
10	4 8 9	3syl	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → ( tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) ↔ tpos 𝐴 : ( 𝐽 × 𝐼 ) ⟶ 𝐵 ) )
11	3 10	mpbird	⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 𝐼 × 𝐽 ) ) → tpos 𝐴 ∈ ( 𝐵 ↑m ( 𝐽 × 𝐼 ) ) )