# 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}\mathrm{Mat}{R}$
mattposcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion mattposcl ${⊢}{M}\in {B}\to tpos{M}\in {B}$

### Proof

Step Hyp Ref Expression
1 mattposcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mattposcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
4 1 3 2 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
5 elmapi ${⊢}{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
6 tposf ${⊢}{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}\to tpos{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
7 4 5 6 3syl ${⊢}{M}\in {B}\to tpos{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
8 fvex ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{V}$
9 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
10 9 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
11 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
12 11 anidms ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{Fin}$
13 10 12 syl ${⊢}{M}\in {B}\to {N}×{N}\in \mathrm{Fin}$
14 elmapg ${⊢}\left({\mathrm{Base}}_{{R}}\in \mathrm{V}\wedge {N}×{N}\in \mathrm{Fin}\right)\to \left(tpos{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)↔tpos{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}\right)$
15 8 13 14 sylancr ${⊢}{M}\in {B}\to \left(tpos{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)↔tpos{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}\right)$
16 7 15 mpbird ${⊢}{M}\in {B}\to tpos{M}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
17 1 3 matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
18 9 17 syl ${⊢}{M}\in {B}\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
19 18 2 eqtr4di ${⊢}{M}\in {B}\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={B}$
20 16 19 eleqtrd ${⊢}{M}\in {B}\to tpos{M}\in {B}$