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 ⊢ A = N Mat R
mattposcl.b ⊢ B = Base A
Assertion mattpostpos ⊢ M ∈ 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 ∈ B → M ∈ Base R N × N
5 elmapi ⊢ M ∈ Base R N × N → M : N × N ⟶ Base R
6 4 5 syl ⊢ M ∈ B → M : N × N ⟶ Base R
7 frel ⊢ M : N × N ⟶ Base R → Rel ⁡ M
8 6 7 syl ⊢ M ∈ B → Rel ⁡ M
9 relxp ⊢ Rel ⁡ N × N
10 6 fdmd ⊢ M ∈ B → dom ⁡ M = N × N
11 10 releqd ⊢ M ∈ B → Rel ⁡ dom ⁡ M ↔ Rel ⁡ N × N
12 9 11 mpbiri ⊢ M ∈ B → Rel ⁡ dom ⁡ M
13 tpostpos2 ⊢ Rel ⁡ M ∧ Rel ⁡ dom ⁡ M → tpos tpos M = M
14 8 12 13 syl2anc ⊢ M ∈ B → tpos tpos M = M