This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( 𝑁 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 𝑀 = 𝑀 )