dmatelnd

Description: An extradiagonal entry of a diagonal matrix is equal to zero. (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	dmatelnd	$⊢ ((N \in Fin \land R \in Ring \land X \in D) \land (I \in N \land J \in N \land I \neq J)) \to I X J = \underset{˙}{0}$

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 2 3 4	dmatel	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \leftrightarrow (X \in B \land \forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0})))$
6		neeq1	$⊢ i = I \to (i \neq j \leftrightarrow I \neq j)$
7		oveq1	$⊢ i = I \to i X j = I X j$
8	7	eqeq1d	$⊢ i = I \to (i X j = \underset{˙}{0} \leftrightarrow I X j = \underset{˙}{0})$
9	6 8	imbi12d	$⊢ i = I \to ((i \neq j \to i X j = \underset{˙}{0}) \leftrightarrow (I \neq j \to I X j = \underset{˙}{0}))$
10		neeq2	$⊢ j = J \to (I \neq j \leftrightarrow I \neq J)$
11		oveq2	$⊢ j = J \to I X j = I X J$
12	11	eqeq1d	$⊢ j = J \to (I X j = \underset{˙}{0} \leftrightarrow I X J = \underset{˙}{0})$
13	10 12	imbi12d	$⊢ j = J \to ((I \neq j \to I X j = \underset{˙}{0}) \leftrightarrow (I \neq J \to I X J = \underset{˙}{0}))$
14	9 13	rspc2v	$⊢ (I \in N \land J \in N) \to (\forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0}) \to (I \neq J \to I X J = \underset{˙}{0}))$
15	14	com23	$⊢ (I \in N \land J \in N) \to (I \neq J \to (\forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0}) \to I X J = \underset{˙}{0}))$
16	15	3impia	$⊢ (I \in N \land J \in N \land I \neq J) \to (\forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0}) \to I X J = \underset{˙}{0})$
17	16	com12	$⊢ \forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0}) \to ((I \in N \land J \in N \land I \neq J) \to I X J = \underset{˙}{0})$
18	17	2a1i	$⊢ (N \in Fin \land R \in Ring) \to (X \in B \to (\forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0}) \to ((I \in N \land J \in N \land I \neq J) \to I X J = \underset{˙}{0})))$
19	18	impd	$⊢ (N \in Fin \land R \in Ring) \to ((X \in B \land \forall i \in N \forall j \in N (i \neq j \to i X j = \underset{˙}{0})) \to ((I \in N \land J \in N \land I \neq J) \to I X J = \underset{˙}{0}))$
20	5 19	sylbid	$⊢ (N \in Fin \land R \in Ring) \to (X \in D \to ((I \in N \land J \in N \land I \neq J) \to I X J = \underset{˙}{0}))$
21	20	3impia	$⊢ (N \in Fin \land R \in Ring \land X \in D) \to ((I \in N \land J \in N \land I \neq J) \to I X J = \underset{˙}{0})$
22	21	imp	$⊢ ((N \in Fin \land R \in Ring \land X \in D) \land (I \in N \land J \in N \land I \neq J)) \to I X J = \underset{˙}{0}$

Metamath Proof Explorer

Theorem dmatelnd

Proof