mdetdiag

Description: The determinant of a diagonal matrix is the product of the entries 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}$
Assertion	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))$

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		simpl3	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to M \in B$
7		eqid	$⊢ {Base}_{SymGrp (N)} = {Base}_{SymGrp (N)}$
8		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
9		eqid	$⊢ pmSgn (N) = pmSgn (N)$
10		eqid	$⊢ \cdot_{R} = \cdot_{R}$
11	1 2 3 7 8 9 10 4	mdetleib	$⊢ M \in B \to D (M) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)))$
12	6 11	syl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to D (M) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)))$
13		simpl1	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to R \in CRing$
14	13	ad2antrr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to R \in CRing$
15	6	ad2antrr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to M \in B$
16		simpr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to p = {I ↾}_{N}$
17	2 3 4 8 9 10	madetsumid	$⊢ (R \in CRing \land M \in B \land p = {I ↾}_{N}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = \underset{k \in N}{\sum_{G}} (k M k)$
18	14 15 16 17	syl3anc	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = \underset{k \in N}{\sum_{G}} (k M k)$
19		iftrue	$⊢ p = {I ↾}_{N} \to if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}) = \underset{k \in N}{\sum_{G}} (k M k)$
20	19	eqcomd	$⊢ p = {I ↾}_{N} \to \underset{k \in N}{\sum_{G}} (k M k) = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
21	20	adantl	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to \underset{k \in N}{\sum_{G}} (k M k) = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
22	18 21	eqtrd	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land p = {I ↾}_{N}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
23		simplll	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to (R \in CRing \land N \in Fin \land M \in B)$
24		simpr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})$
25	24	ad2antrr	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})$
26		simpr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \to p \in {Base}_{SymGrp (N)}$
27		neqne	$⊢ \neg p = {I ↾}_{N} \to p \neq {I ↾}_{N}$
28	26 27	anim12i	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to (p \in {Base}_{SymGrp (N)} \land p \neq {I ↾}_{N})$
29	1 2 3 4 5 7 8 9 10	mdetdiaglem	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0}) \land (p \in {Base}_{SymGrp (N)} \land p \neq {I ↾}_{N})) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = \underset{˙}{0}$
30	23 25 28 29	syl3anc	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = \underset{˙}{0}$
31		iffalse	$⊢ \neg p = {I ↾}_{N} \to if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}) = \underset{˙}{0}$
32	31	adantl	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}) = \underset{˙}{0}$
33	32	eqcomd	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to \underset{˙}{0} = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
34	30 33	eqtrd	$⊢ ((((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \land \neg p = {I ↾}_{N}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
35	22 34	pm2.61dan	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land p \in {Base}_{SymGrp (N)}) \to (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k)) = if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
36	35	mpteq2dva	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to (p \in {Base}_{SymGrp (N)} ⟼ (ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k))) = (p \in {Base}_{SymGrp (N)} ⟼ if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}))$
37	36	oveq2d	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} ((ℤRHom (R) \circ pmSgn (N)) (p) \cdot_{R} (\underset{k \in N}{\sum_{G}}, (p (k) M k))) = \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})$
38		crngring	$⊢ R \in CRing \to R \in Ring$
39		ringmnd	$⊢ R \in Ring \to R \in Mnd$
40	38 39	syl	$⊢ R \in CRing \to R \in Mnd$
41	40	3ad2ant1	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to R \in Mnd$
42	41	adantr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to R \in Mnd$
43		fvexd	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to {Base}_{SymGrp (N)} \in V$
44		eqid	$⊢ SymGrp (N) = SymGrp (N)$
45	44	symgid	$⊢ N \in Fin \to {I ↾}_{N} = 0_{SymGrp (N)}$
46	45	3ad2ant2	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to {I ↾}_{N} = 0_{SymGrp (N)}$
47	44	symggrp	$⊢ N \in Fin \to SymGrp (N) \in Grp$
48	47	3ad2ant2	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to SymGrp (N) \in Grp$
49		eqid	$⊢ 0_{SymGrp (N)} = 0_{SymGrp (N)}$
50	7 49	grpidcl	$⊢ SymGrp (N) \in Grp \to 0_{SymGrp (N)} \in {Base}_{SymGrp (N)}$
51	48 50	syl	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to 0_{SymGrp (N)} \in {Base}_{SymGrp (N)}$
52	46 51	eqeltrd	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to {I ↾}_{N} \in {Base}_{SymGrp (N)}$
53	52	adantr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to {I ↾}_{N} \in {Base}_{SymGrp (N)}$
54		eqid	$⊢ (p \in {Base}_{SymGrp (N)} ⟼ if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0})) = (p \in {Base}_{SymGrp (N)} ⟼ if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}))$
55		eqid	$⊢ {Base}_{R} = {Base}_{R}$
56	4 55	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
57	4	crngmgp	$⊢ R \in CRing \to G \in CMnd$
58	57	3ad2ant1	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to G \in CMnd$
59	58	adantr	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to G \in CMnd$
60		simpl2	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to N \in Fin$
61		simpr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land k \in N) \to k \in N$
62	3	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
63	62	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
64	63	3ad2ant3	$⊢ (R \in CRing \land N \in Fin \land M \in B) \to M \in {Base}_{A}$
65	64	ad2antrr	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land k \in N) \to M \in {Base}_{A}$
66	2 55	matecl	$⊢ (k \in N \land k \in N \land M \in {Base}_{A}) \to k M k \in {Base}_{R}$
67	61 61 65 66	syl3anc	$⊢ (((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \land k \in N) \to k M k \in {Base}_{R}$
68	67	ralrimiva	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \forall k \in N k M k \in {Base}_{R}$
69	56 59 60 68	gsummptcl	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \underset{k \in N}{\sum_{G}} (k M k) \in {Base}_{R}$
70	5 42 43 53 54 69	gsummptif1n0	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \forall i \in N \forall j \in N (i \neq j \to i M j = \underset{˙}{0})) \to \underset{p \in {Base}_{SymGrp (N)}}{\sum_{R}} if (p = {I ↾}_{N}, \underset{k \in N}{\sum_{G}} (k M k), \underset{˙}{0}) = \underset{k \in N}{\sum_{G}} (k M k)$
71	12 37 70	3eqtrd	$⊢ ((R \in CRing \land N \in Fin \land M \in B) \land \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)$
72	71	ex	$⊢ (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))$

Metamath Proof Explorer

Theorem mdetdiag

Proof