mdetdiagid

Description: The determinant of a diagonal matrix with identical entries is the power of the entry in the diagonal. (Contributed by AV, 17-Aug-2019)

	Ref	Expression
Hypotheses	mdetdiag.d	$⊢ D = N maDet R$
	mdetdiag.a	$⊢ A = N Mat R$
	mdetdiag.b	$⊢ B = {Base}_{A}$
	mdetdiag.g	$⊢ G = {mulGrp}_{R}$
	mdetdiag.0	$⊢ \underset{˙}{0} = 0_{R}$
	mdetdiagid.c	$⊢ C = {Base}_{R}$
	mdetdiagid.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mdetdiagid	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to D (M) = \|N\| \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		mdetdiag.d	$⊢ D = N maDet R$
2		mdetdiag.a	$⊢ A = N Mat R$
3		mdetdiag.b	$⊢ B = {Base}_{A}$
4		mdetdiag.g	$⊢ G = {mulGrp}_{R}$
5		mdetdiag.0	$⊢ \underset{˙}{0} = 0_{R}$
6		mdetdiagid.c	$⊢ C = {Base}_{R}$
7		mdetdiagid.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
8		simpl	$⊢ (R \in CRing \land N \in Fin) \to R \in CRing$
9	8	adantr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to R \in CRing$
10		simpr	$⊢ (R \in CRing \land N \in Fin) \to N \in Fin$
11	10	adantr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to N \in Fin$
12		simpl	$⊢ (M \in B \land X \in C) \to M \in B$
13	12	adantl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to M \in B$
14	9 11 13	3jca	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to (R \in CRing \land N \in Fin \land M \in B)$
15	14	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to (R \in CRing \land N \in Fin \land M \in B)$
16		id	$⊢ i M j = if (i = j, X, \underset{˙}{0}) \to i M j = if (i = j, X, \underset{˙}{0})$
17		ifnefalse	$⊢ i \neq j \to if (i = j, X, \underset{˙}{0}) = \underset{˙}{0}$
18	17	adantl	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land i \in N) \land j \in N) \land i \neq j) \to if (i = j, X, \underset{˙}{0}) = \underset{˙}{0}$
19	16 18	sylan9eqr	$⊢ ((((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land i \in N) \land j \in N) \land i \neq j) \land i M j = if (i = j, X, \underset{˙}{0})) \to i M j = \underset{˙}{0}$
20	19	exp31	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land i \in N) \land j \in N) \to (i \neq j \to (i M j = if (i = j, X, \underset{˙}{0}) \to i M j = \underset{˙}{0}))$
21	20	com23	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land i \in N) \land j \in N) \to (i M j = if (i = j, X, \underset{˙}{0}) \to (i \neq j \to i M j = \underset{˙}{0}))$
22	21	ralimdva	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land i \in N) \to (\forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to \forall j \in N (i \neq j \to i M j = \underset{˙}{0}))$
23	22	ralimdva	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}))$
24	23	imp	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})$
25	1 2 3 4 5	mdetdiag	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to (\forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \to D (M) = \underset{k \in N}{\sum_{G}} (k M k))$
26	15 24 25	sylc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to D (M) = \underset{k \in N}{\sum_{G}} (k M k)$
27		oveq1	$⊢ i = k \to i M j = k M j$
28		equequ1	$⊢ i = k \to (i = j \leftrightarrow k = j)$
29	28	ifbid	$⊢ i = k \to if (i = j, X, \underset{˙}{0}) = if (k = j, X, \underset{˙}{0})$
30	27 29	eqeq12d	$⊢ i = k \to (i M j = if (i = j, X, \underset{˙}{0}) \leftrightarrow k M j = if (k = j, X, \underset{˙}{0}))$
31		oveq2	$⊢ j = k \to k M j = k M k$
32		equequ2	$⊢ j = k \to (k = j \leftrightarrow k = k)$
33	32	ifbid	$⊢ j = k \to if (k = j, X, \underset{˙}{0}) = if (k = k, X, \underset{˙}{0})$
34	31 33	eqeq12d	$⊢ j = k \to (k M j = if (k = j, X, \underset{˙}{0}) \leftrightarrow k M k = if (k = k, X, \underset{˙}{0}))$
35	30 34	rspc2v	$⊢ (k \in N \land k \in N) \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to k M k = if (k = k, X, \underset{˙}{0}))$
36	35	anidms	$⊢ k \in N \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to k M k = if (k = k, X, \underset{˙}{0}))$
37	36	adantl	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land k \in N) \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to k M k = if (k = k, X, \underset{˙}{0}))$
38	37	imp	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land k \in N) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to k M k = if (k = k, X, \underset{˙}{0})$
39		equid	$⊢ k = k$
40	39	iftruei	$⊢ if (k = k, X, \underset{˙}{0}) = X$
41	38 40	eqtrdi	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land k \in N) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to k M k = X$
42	41	an32s	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \land k \in N) \to k M k = X$
43	42	mpteq2dva	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to (k \in N ⟼ k M k) = (k \in N ⟼ X)$
44	43	oveq2d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to \underset{k \in N}{\sum_{G}} (k M k) = \underset{k \in N}{\sum_{G}} X$
45	4	crngmgp	$⊢ R \in CRing \to G \in CMnd$
46		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
47	45 46	syl	$⊢ R \in CRing \to G \in Mnd$
48	47	adantr	$⊢ (R \in CRing \land N \in Fin) \to G \in Mnd$
49		simpr	$⊢ (M \in B \land X \in C) \to X \in C$
50	4 6	mgpbas	$⊢ C = {Base}_{G}$
51	50 7	gsumconst	$⊢ (G \in Mnd \land N \in Fin \land X \in C) \to \underset{k \in N}{\sum_{G}} X = \|N\| \underset{˙}{\cdot} X$
52	48 10 49 51	syl2an3an	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to \underset{k \in N}{\sum_{G}} X = \|N\| \underset{˙}{\cdot} X$
53	52	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to \underset{k \in N}{\sum_{G}} X = \|N\| \underset{˙}{\cdot} X$
54	26 44 53	3eqtrd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \land \forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0})) \to D (M) = \|N\| \underset{˙}{\cdot} X$
55	54	ex	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land X \in C)) \to (\forall i \in N \forall j \in N i M j = if (i = j, X, \underset{˙}{0}) \to D (M) = \|N\| \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mdetdiagid

Proof