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 Mat R
mattpos1.o ⊢ 1 ˙ = 1 A
Assertion mattpos1 ⊢ N ∈ Fin ∧ R ∈ Ring → tpos 1 ˙ = 1 ˙

Proof

Step Hyp Ref Expression
1 mattpos1.a ⊢ A = N Mat R
2 mattpos1.o ⊢ 1 ˙ = 1 A
3 eqid ⊢ i ∈ N , j ∈ N ⟼ if i = j 1 R 0 R = i ∈ N , j ∈ N ⟼ if i = j 1 R 0 R
4 3 tposmpo ⊢ tpos i ∈ N , j ∈ N ⟼ if i = j 1 R 0 R = j ∈ N , i ∈ N ⟼ if i = j 1 R 0 R
5 eqid ⊢ 1 R = 1 R
6 eqid ⊢ 0 R = 0 R
7 1 5 6 mat1 ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 R 0 R
8 7 tposeqd ⊢ N ∈ Fin ∧ R ∈ Ring → tpos 1 A = tpos i ∈ N , j ∈ N ⟼ if i = j 1 R 0 R
9 1 5 6 mat1 ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = j ∈ N , i ∈ N ⟼ if j = i 1 R 0 R
10 equcom ⊢ j = i ↔ i = j
11 10 a1i ⊢ j ∈ N ∧ i ∈ N → j = i ↔ i = j
12 11 ifbid ⊢ j ∈ N ∧ i ∈ N → if j = i 1 R 0 R = if i = j 1 R 0 R
13 12 mpoeq3ia ⊢ j ∈ N , i ∈ N ⟼ if j = i 1 R 0 R = j ∈ N , i ∈ N ⟼ if i = j 1 R 0 R
14 9 13 eqtrdi ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = j ∈ N , i ∈ N ⟼ if i = j 1 R 0 R
15 4 8 14 3eqtr4a ⊢ N ∈ Fin ∧ R ∈ Ring → tpos 1 A = 1 A
16 2 tposeqi ⊢ tpos 1 ˙ = tpos 1 A
17 15 16 2 3eqtr4g ⊢ N ∈ Fin ∧ R ∈ Ring → tpos 1 ˙ = 1 ˙