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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mattposcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	mattpostpos	⊢ ( 𝑀 ∈ 𝐵 → tpos tpos 𝑀 = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mattposcl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mattposcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	1 3 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
5		elmapi	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
6	4 5	syl	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
7		frel	⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) → Rel 𝑀 )
8	6 7	syl	⊢ ( 𝑀 ∈ 𝐵 → Rel 𝑀 )
9		relxp	⊢ Rel ( 𝑁 × 𝑁 )
10	6	fdmd	⊢ ( 𝑀 ∈ 𝐵 → dom 𝑀 = ( 𝑁 × 𝑁 ) )
11	10	releqd	⊢ ( 𝑀 ∈ 𝐵 → ( Rel dom 𝑀 ↔ Rel ( 𝑁 × 𝑁 ) ) )
12	9 11	mpbiri	⊢ ( 𝑀 ∈ 𝐵 → Rel dom 𝑀 )
13		tpostpos2	⊢ ( ( Rel 𝑀 ∧ Rel dom 𝑀 ) → tpos tpos 𝑀 = 𝑀 )
14	8 12 13	syl2anc	⊢ ( 𝑀 ∈ 𝐵 → tpos tpos 𝑀 = 𝑀 )