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 ( 𝐽 × 𝐼 ) ) )