Metamath Proof Explorer

Theorem mattpostpos

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

Ref Expression
Hypotheses mattposcl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mattposcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion mattpostpos ${⊢}{M}\in {B}\to tpostpos{M}={M}$

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 4 5 syl ${⊢}{M}\in {B}\to {M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}$
7 frel ${⊢}{M}:{N}×{N}⟶{\mathrm{Base}}_{{R}}\to \mathrm{Rel}{M}$
8 6 7 syl ${⊢}{M}\in {B}\to \mathrm{Rel}{M}$
9 relxp ${⊢}\mathrm{Rel}\left({N}×{N}\right)$
10 6 fdmd ${⊢}{M}\in {B}\to \mathrm{dom}{M}={N}×{N}$
11 10 releqd ${⊢}{M}\in {B}\to \left(\mathrm{Rel}\mathrm{dom}{M}↔\mathrm{Rel}\left({N}×{N}\right)\right)$
12 9 11 mpbiri ${⊢}{M}\in {B}\to \mathrm{Rel}\mathrm{dom}{M}$
13 tpostpos2 ${⊢}\left(\mathrm{Rel}{M}\wedge \mathrm{Rel}\mathrm{dom}{M}\right)\to tpostpos{M}={M}$
14 8 12 13 syl2anc ${⊢}{M}\in {B}\to tpostpos{M}={M}$