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