mat1

Description: Value of an identity matrix, see also the statement in Lang p. 504: "The unit element of the ring of n x n matrices is the matrix I_n ... whose components are equal to 0 except on the diagonal, in which case they are equal to 1.". (Contributed by Stefan O'Rear, 7-Sep-2015)

	Ref	Expression
Hypotheses	mat1.a	$⊢ A = N Mat R$
	mat1.o	$⊢ \underset{˙}{1} = 1_{R}$
	mat1.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	mat1	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$

Proof

Step	Hyp	Ref	Expression
1		mat1.a	$⊢ A = N Mat R$
2		mat1.o	$⊢ \underset{˙}{1} = 1_{R}$
3		mat1.z	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
6		eqid	$⊢ (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$
7		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
8	4 5 2 3 6 7	mamumat1cl	$⊢ (N \in Fin \land R \in Ring) \to (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \in ({Base}_{R}^{(N \times N)})$
9	1 4	matbas2	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
10	8 9	eleqtrd	$⊢ (N \in Fin \land R \in Ring) \to (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \in {Base}_{A}$
11		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
12	1 11	matmulr	$⊢ (N \in Fin \land R \in Ring) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
13	12	adantr	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
14	13	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) (R maMul ⟨N, N, N⟩) x = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x$
15		simplr	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to R \in Ring$
16		simpll	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to N \in Fin$
17	9	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (x \in ({Base}_{R}^{(N \times N)}) \leftrightarrow x \in {Base}_{A})$
18	17	biimpar	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to x \in ({Base}_{R}^{(N \times N)})$
19	4 15 2 3 6 16 16 11 18	mamulid	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) (R maMul ⟨N, N, N⟩) x = x$
20	14 19	eqtr3d	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x = x$
21	13	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to x (R maMul ⟨N, N, N⟩) (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$
22	4 15 2 3 6 16 16 11 18	mamurid	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to x (R maMul ⟨N, N, N⟩) (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x$
23	21 22	eqtr3d	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x$
24	20 23	jca	$⊢ ((N \in Fin \land R \in Ring) \land x \in {Base}_{A}) \to ((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x = x \land x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x)$
25	24	ralrimiva	$⊢ (N \in Fin \land R \in Ring) \to \forall x \in {Base}_{A} ((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x = x \land x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x)$
26	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
27		eqid	$⊢ {Base}_{A} = {Base}_{A}$
28		eqid	$⊢ \cdot_{A} = \cdot_{A}$
29		eqid	$⊢ 1_{A} = 1_{A}$
30	27 28 29	isringid	$⊢ A \in Ring \to (((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \in {Base}_{A} \land \forall x \in {Base}_{A} ((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x = x \land x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x)) \leftrightarrow 1_{A} = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})))$
31	26 30	syl	$⊢ (N \in Fin \land R \in Ring) \to (((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \in {Base}_{A} \land \forall x \in {Base}_{A} ((i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) \cdot_{A} x = x \land x \cdot_{A} (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})) = x)) \leftrightarrow 1_{A} = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0})))$
32	10 25 31	mpbi2and	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} = (i \in N, j \in N ⟼ if (i = j, \underset{˙}{1}, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem mat1

Proof