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 Mat R )
	mattposcl.b	|- B = ( Base ` A )
Assertion	mattpostpos	|- ( M e. B -> tpos tpos M = M )

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 e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
5		elmapi	|- ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
6	4 5	syl	|- ( M e. B -> M : ( N X. N ) --> ( Base ` R ) )
7		frel	|- ( M : ( N X. N ) --> ( Base ` R ) -> Rel M )
8	6 7	syl	|- ( M e. B -> Rel M )
9		relxp	|- Rel ( N X. N )
10	6	fdmd	|- ( M e. B -> dom M = ( N X. N ) )
11	10	releqd	|- ( M e. B -> ( Rel dom M <-> Rel ( N X. N ) ) )
12	9 11	mpbiri	|- ( M e. B -> Rel dom M )
13		tpostpos2	|- ( ( Rel M /\ Rel dom M ) -> tpos tpos M = M )
14	8 12 13	syl2anc	|- ( M e. B -> tpos tpos M = M )