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 )