dmatid

Description: The identity matrix is a diagonal matrix. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	dmatid.a	$⊢ A = N Mat R$
	dmatid.b	$⊢ B = {Base}_{A}$
	dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
	dmatid.d	$⊢ D = N DMat R$
Assertion	dmatid	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in D$

Proof

Step	Hyp	Ref	Expression
1		dmatid.a	$⊢ A = N Mat R$
2		dmatid.b	$⊢ B = {Base}_{A}$
3		dmatid.0	$⊢ \underset{˙}{0} = 0_{R}$
4		dmatid.d	$⊢ D = N DMat R$
5	1	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
6		eqid	$⊢ 1_{A} = 1_{A}$
7	2 6	ringidcl	$⊢ A \in Ring \to 1_{A} \in B$
8	5 7	syl	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in B$
9		eqid	$⊢ 1_{R} = 1_{R}$
10		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
11	10	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to N \in Fin$
12		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
13	12	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to R \in Ring$
14		simpl	$⊢ (i \in N \land j \in N) \to i \in N$
15	14	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i \in N$
16		simpr	$⊢ (i \in N \land j \in N) \to j \in N$
17	16	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to j \in N$
18	1 9 3 11 13 15 17 6	mat1ov	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to i 1_{A} j = if (i = j, 1_{R}, \underset{˙}{0})$
19		ifnefalse	$⊢ i \neq j \to if (i = j, 1_{R}, \underset{˙}{0}) = \underset{˙}{0}$
20	18 19	sylan9eq	$⊢ (((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \land i \neq j) \to i 1_{A} j = \underset{˙}{0}$
21	20	ex	$⊢ ((N \in Fin \land R \in Ring) \land (i \in N \land j \in N)) \to (i \neq j \to i 1_{A} j = \underset{˙}{0})$
22	21	ralrimivva	$⊢ (N \in Fin \land R \in Ring) \to \forall i \in N \forall j \in N (i \neq j \to i 1_{A} j = \underset{˙}{0})$
23	1 2 3 4	dmatel	$⊢ (N \in Fin \land R \in Ring) \to (1_{A} \in D \leftrightarrow (1_{A} \in B \land \forall i \in N \forall j \in N (i \neq j \to i 1_{A} j = \underset{˙}{0})))$
24	8 22 23	mpbir2and	$⊢ (N \in Fin \land R \in Ring) \to 1_{A} \in D$

Metamath Proof Explorer

Theorem dmatid

Proof