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 ⊢ A = N Mat R
mattposcl.b ⊢ B = Base A
Assertion mattposcl ⊢ M ∈ B → tpos M ∈ B

Proof

Step Hyp Ref Expression
1 mattposcl.a ⊢ A = N Mat R
2 mattposcl.b ⊢ B = Base A
3 eqid ⊢ Base R = Base R
4 1 3 2 matbas2i ⊢ M ∈ B → M ∈ Base R N × N
5 elmapi ⊢ M ∈ Base R N × N → M : N × N ⟶ Base R
6 tposf ⊢ M : N × N ⟶ Base R → tpos M : N × N ⟶ Base R
7 4 5 6 3syl ⊢ M ∈ B → tpos M : N × N ⟶ Base R
8 fvex ⊢ Base R ∈ V
9 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
10 9 simpld ⊢ M ∈ B → N ∈ Fin
11 xpfi ⊢ N ∈ Fin ∧ N ∈ Fin → N × N ∈ Fin
12 11 anidms ⊢ N ∈ Fin → N × N ∈ Fin
13 10 12 syl ⊢ M ∈ B → N × N ∈ Fin
14 elmapg ⊢ Base R ∈ V ∧ N × N ∈ Fin → tpos M ∈ Base R N × N ↔ tpos M : N × N ⟶ Base R
15 8 13 14 sylancr ⊢ M ∈ B → tpos M ∈ Base R N × N ↔ tpos M : N × N ⟶ Base R
16 7 15 mpbird ⊢ M ∈ B → tpos M ∈ Base R N × N
17 1 3 matbas2 ⊢ N ∈ Fin ∧ R ∈ V → Base R N × N = Base A
18 9 17 syl ⊢ M ∈ B → Base R N × N = Base A
19 18 2 eqtr4di ⊢ M ∈ B → Base R N × N = B
20 16 19 eleqtrd ⊢ M ∈ B → tpos M ∈ B