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	$⊢ \underset{˙}{1} = 1_{A}$
Assertion	mattpos1	$⊢ (N \in Fin \land R \in Ring) \to tpos \underset{˙}{1} = \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		mattpos1.a	$⊢ A = N Mat R$
2		mattpos1.o	$⊢ \underset{˙}{1} = 1_{A}$
3		eqid	$⊢ (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R})) = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
4	3	tposmpo	$⊢ tpos (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R})) = (j \in N, i \in 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 \in Fin \land R \in Ring) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
8	7	tposeqd	$⊢ (N \in Fin \land R \in Ring) \to tpos 1_{A} = tpos (i \in N, j \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
9	1 5 6	mat1	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (j \in N, i \in N ⟼ if (j = i, 1_{R}, 0_{R}))$
10		equcom	$⊢ j = i \leftrightarrow i = j$
11	10	a1i	$⊢ (j \in N \land i \in N) \to (j = i \leftrightarrow i = j)$
12	11	ifbid	$⊢ (j \in N \land i \in N) \to if (j = i, 1_{R}, 0_{R}) = if (i = j, 1_{R}, 0_{R})$
13	12	mpoeq3ia	$⊢ (j \in N, i \in N ⟼ if (j = i, 1_{R}, 0_{R})) = (j \in N, i \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
14	9 13	eqtrdi	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (j \in N, i \in N ⟼ if (i = j, 1_{R}, 0_{R}))$
15	4 8 14	3eqtr4a	$⊢ (N \in Fin \land R \in Ring) \to tpos 1_{A} = 1_{A}$
16	2	tposeqi	$⊢ tpos \underset{˙}{1} = tpos 1_{A}$
17	15 16 2	3eqtr4g	$⊢ (N \in Fin \land R \in Ring) \to tpos \underset{˙}{1} = \underset{˙}{1}$

Metamath Proof Explorer