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 tposM\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\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		tposf	$$⊢M:N\times N⟶{\mathrm{Base}}_R\to tposM:N\times N⟶{\mathrm{Base}}_R$$
7	4 5 6	3syl	$$⊢M\in B\to tposM:N\times 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\times N\in \mathrm{Fin}$$
12	11	anidms	$$⊢N\in \mathrm{Fin}\to N\times N\in \mathrm{Fin}$$
13	10 12	syl	$$⊢M\in B\to N\times N\in \mathrm{Fin}$$
14		elmapg	$$⊢\left({\mathrm{Base}}_R\in \mathrm{V}\wedge N\times N\in \mathrm{Fin}\right)\to \left(tposM\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\leftrightarrow tposM:N\times N⟶{\mathrm{Base}}_R\right)$$
15	8 13 14	sylancr	$$⊢M\in B\to \left(tposM\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)\leftrightarrow tposM:N\times N⟶{\mathrm{Base}}_R\right)$$
16	7 15	mpbird	$$⊢M\in B\to tposM\in \left({{\mathrm{Base}}_R}^{\left(N\times N\right)}\right)$$
17	1 3	matbas2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {{\mathrm{Base}}_R}^{\left(N\times N\right)}={\mathrm{Base}}_A$$
18	9 17	syl	$$⊢M\in B\to {{\mathrm{Base}}_R}^{\left(N\times N\right)}={\mathrm{Base}}_A$$
19	18 2	eqtr4di	$$⊢M\in B\to {{\mathrm{Base}}_R}^{\left(N\times N\right)}=B$$
20	16 19	eleqtrd	$$⊢M\in B\to tposM\in B$$