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 tpostposM=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\times N\right)}\right)$$
5		elmapi	$$⊢M\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\to M:N\times N⟶{\mathrm{Base}}_R$$
6	4 5	syl	$$⊢M\in B\to M:N\times N⟶{\mathrm{Base}}_R$$
7		frel	$$⊢M:N\times 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\times N\right)$$
10	6	fdmd	$$⊢M\in B\to \mathrm{dom}M=N\times N$$
11	10	releqd	$$⊢M\in B\to \left(\mathrm{Rel}\mathrm{dom}M\leftrightarrow \mathrm{Rel}\left(N\times 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 tpostposM=M$$
14	8 12 13	syl2anc	$$⊢M\in B\to tpostposM=M$$