This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mattposcl

Description: The transpose of a square matrix is a square matrix of the same size. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses mattposcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mattposcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion mattposcl ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 mattposcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mattposcl.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 1 3 2 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
5 elmapi ⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
6 tposf ⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
7 4 5 6 3syl ⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
8 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
9 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10 9 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
11 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
12 11 anidms ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
13 10 12 syl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 × 𝑁 ) ∈ Fin )
14 elmapg ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( 𝑁 × 𝑁 ) ∈ Fin ) → ( tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ) )
15 8 13 14 sylancr ⊢ ( 𝑀 ∈ 𝐵 → ( tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) ↔ tpos 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) ) )
16 7 15 mpbird ⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
17 1 3 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
18 9 17 syl ⊢ ( 𝑀 ∈ 𝐵 → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
19 18 2 eqtr4di ⊢ ( 𝑀 ∈ 𝐵 → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = 𝐵 )
20 16 19 eleqtrd ⊢ ( 𝑀 ∈ 𝐵 → tpos 𝑀 ∈ 𝐵 )