# Metamath Proof Explorer

## Theorem mattpos1

Description: The transposition of the identity matrix is the identity matrix. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Hypotheses mattpos1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mattpos1.o
Assertion mattpos1

### Proof

Step Hyp Ref Expression
1 mattpos1.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mattpos1.o
3 eqid ${⊢}\left({i}\in {N},{j}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)=\left({i}\in {N},{j}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
4 3 tposmpo ${⊢}tpos\left({i}\in {N},{j}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)=\left({j}\in {N},{i}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
5 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
6 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
7 1 5 6 mat1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{A}}=\left({i}\in {N},{j}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
8 7 tposeqd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to tpos{1}_{{A}}=tpos\left({i}\in {N},{j}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
9 1 5 6 mat1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{A}}=\left({j}\in {N},{i}\in {N}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)$
10 equcom ${⊢}{j}={i}↔{i}={j}$
11 10 a1i ${⊢}\left({j}\in {N}\wedge {i}\in {N}\right)\to \left({j}={i}↔{i}={j}\right)$
12 11 ifbid ${⊢}\left({j}\in {N}\wedge {i}\in {N}\right)\to if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)=if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)$
13 12 mpoeq3ia ${⊢}\left({j}\in {N},{i}\in {N}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)=\left({j}\in {N},{i}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
14 9 13 eqtrdi ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{A}}=\left({j}\in {N},{i}\in {N}⟼if\left({i}={j},{1}_{{R}},{0}_{{R}}\right)\right)$
15 4 8 14 3eqtr4a ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to tpos{1}_{{A}}={1}_{{A}}$
16 2 tposeqi
17 15 16 2 3eqtr4g