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

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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mattpos1.o ⊢ 1 = ( 1r ‘ 𝐴 )
Assertion mattpos1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → tpos 1 = 1 )

Proof

Step Hyp Ref Expression
1 mattpos1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mattpos1.o ⊢ 1 = ( 1r ‘ 𝐴 )
3 eqid ⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
4 3 tposmpo ⊢ tpos ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7 1 5 6 mat1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
8 7 tposeqd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → tpos ( 1r ‘ 𝐴 ) = tpos ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
9 1 5 6 mat1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
10 equcom ⊢ ( 𝑗 = 𝑖 ↔ 𝑖 = 𝑗 )
11 10 a1i ⊢ ( ( 𝑗 ∈ 𝑁 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑗 = 𝑖 ↔ 𝑖 = 𝑗 ) )
12 11 ifbid ⊢ ( ( 𝑗 ∈ 𝑁 ∧ 𝑖 ∈ 𝑁 ) → if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
13 12 mpoeq3ia ⊢ ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑗 = 𝑖 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
14 9 13 eqtrdi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑗 ∈ 𝑁 , 𝑖 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
15 4 8 14 3eqtr4a ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → tpos ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 ) )
16 2 tposeqi ⊢ tpos 1 = tpos ( 1r ‘ 𝐴 )
17 15 16 2 3eqtr4g ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → tpos 1 = 1 )