mdetleib2

Description: Leibniz' formula can also be expanded by rows. (Contributed by Stefan O'Rear, 9-Jul-2018) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	mdetfval.d	$⊢ D = N maDet R$
	mdetfval.a	$⊢ A = N Mat R$
	mdetfval.b	$⊢ B = {Base}_{A}$
	mdetfval.p	$⊢ P = {Base}_{SymGrp (N)}$
	mdetfval.y	$⊢ Y = ℤRHom (R)$
	mdetfval.s	$⊢ S = pmSgn (N)$
	mdetfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetfval.u	$⊢ U = {mulGrp}_{R}$
Assertion	mdetleib2	$⊢ (R \in CRing \land M \in B) \to D (M) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x))))$

Proof

Step	Hyp	Ref	Expression
1		mdetfval.d	$⊢ D = N maDet R$
2		mdetfval.a	$⊢ A = N Mat R$
3		mdetfval.b	$⊢ B = {Base}_{A}$
4		mdetfval.p	$⊢ P = {Base}_{SymGrp (N)}$
5		mdetfval.y	$⊢ Y = ℤRHom (R)$
6		mdetfval.s	$⊢ S = pmSgn (N)$
7		mdetfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetfval.u	$⊢ U = {mulGrp}_{R}$
9	1 2 3 4 5 6 7 8	mdetleib	$⊢ M \in B \to D (M) = \underset{q \in P}{\sum_{R}} ((Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)))$
10	9	adantl	$⊢ (R \in CRing \land M \in B) \to D (M) = \underset{q \in P}{\sum_{R}} ((Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)))$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12		crngring	$⊢ R \in CRing \to R \in Ring$
13		ringcmn	$⊢ R \in Ring \to R \in CMnd$
14	12 13	syl	$⊢ R \in CRing \to R \in CMnd$
15	14	adantr	$⊢ (R \in CRing \land M \in B) \to R \in CMnd$
16	2 3	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
17	16	adantl	$⊢ (R \in CRing \land M \in B) \to (N \in Fin \land R \in V)$
18	17	simpld	$⊢ (R \in CRing \land M \in B) \to N \in Fin$
19		eqid	$⊢ SymGrp (N) = SymGrp (N)$
20	19 4	symgbasfi	$⊢ N \in Fin \to P \in Fin$
21	18 20	syl	$⊢ (R \in CRing \land M \in B) \to P \in Fin$
22	12	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to R \in Ring$
23	5 6	coeq12i	$⊢ Y \circ S = ℤRHom (R) \circ pmSgn (N)$
24		zrhpsgnmhm	$⊢ (R \in Ring \land N \in Fin) \to ℤRHom (R) \circ pmSgn (N) \in (SymGrp (N) MndHom {mulGrp}_{R})$
25	23 24	eqeltrid	$⊢ (R \in Ring \land N \in Fin) \to Y \circ S \in (SymGrp (N) MndHom {mulGrp}_{R})$
26	12 18 25	syl2an2r	$⊢ (R \in CRing \land M \in B) \to Y \circ S \in (SymGrp (N) MndHom {mulGrp}_{R})$
27		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
28	27 11	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
29	4 28	mhmf	$⊢ Y \circ S \in (SymGrp (N) MndHom {mulGrp}_{R}) \to (Y \circ S) : P ⟶ {Base}_{R}$
30	26 29	syl	$⊢ (R \in CRing \land M \in B) \to (Y \circ S) : P ⟶ {Base}_{R}$
31	30	ffvelcdmda	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to (Y \circ S) (q) \in {Base}_{R}$
32	8 11	mgpbas	$⊢ {Base}_{R} = {Base}_{U}$
33	8	crngmgp	$⊢ R \in CRing \to U \in CMnd$
34	33	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to U \in CMnd$
35	18	adantr	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to N \in Fin$
36		simpr	$⊢ (R \in CRing \land M \in B) \to M \in B$
37	2 11 3	matbas2i	$⊢ M \in B \to M \in ({Base}_{R}^{(N \times N)})$
38		elmapi	$⊢ M \in ({Base}_{R}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{R}$
39	36 37 38	3syl	$⊢ (R \in CRing \land M \in B) \to M : N \times N ⟶ {Base}_{R}$
40	39	ad2antrr	$⊢ (((R \in CRing \land M \in B) \land q \in P) \land y \in N) \to M : N \times N ⟶ {Base}_{R}$
41	19 4	symgbasf1o	$⊢ q \in P \to q : N \underset{1-1 onto}{⟶} N$
42	41	adantl	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to q : N \underset{1-1 onto}{⟶} N$
43		f1of	$⊢ q : N \underset{1-1 onto}{⟶} N \to q : N ⟶ N$
44	42 43	syl	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to q : N ⟶ N$
45	44	ffvelcdmda	$⊢ (((R \in CRing \land M \in B) \land q \in P) \land y \in N) \to q (y) \in N$
46		simpr	$⊢ (((R \in CRing \land M \in B) \land q \in P) \land y \in N) \to y \in N$
47	40 45 46	fovcdmd	$⊢ (((R \in CRing \land M \in B) \land q \in P) \land y \in N) \to q (y) M y \in {Base}_{R}$
48	47	ralrimiva	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to \forall y \in N q (y) M y \in {Base}_{R}$
49	32 34 35 48	gsummptcl	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to \underset{y \in N}{\sum_{U}} (q (y) M y) \in {Base}_{R}$
50	11 7	ringcl	$⊢ (R \in Ring \land (Y \circ S) (q) \in {Base}_{R} \land \underset{y \in N}{\sum_{U}} (q (y) M y) \in {Base}_{R}) \to (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)) \in {Base}_{R}$
51	22 31 49 50	syl3anc	$⊢ ((R \in CRing \land M \in B) \land q \in P) \to (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)) \in {Base}_{R}$
52	51	ralrimiva	$⊢ (R \in CRing \land M \in B) \to \forall q \in P (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)) \in {Base}_{R}$
53		eqid	$⊢ (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) = (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)))$
54		eqid	$⊢ {inv}_{g} (SymGrp (N)) = {inv}_{g} (SymGrp (N))$
55	19	symggrp	$⊢ N \in Fin \to SymGrp (N) \in Grp$
56	18 55	syl	$⊢ (R \in CRing \land M \in B) \to SymGrp (N) \in Grp$
57	4 54 56	grpinvf1o	$⊢ (R \in CRing \land M \in B) \to {inv}_{g} (SymGrp (N)) : P \underset{1-1 onto}{⟶} P$
58	11 15 21 52 53 57	gsummptfif1o	$⊢ (R \in CRing \land M \in B) \to \underset{q \in P}{\sum_{R}} ((Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) = \sum_{R} ((q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) \circ {inv}_{g} (SymGrp (N)))$
59		f1of	$⊢ {inv}_{g} (SymGrp (N)) : P \underset{1-1 onto}{⟶} P \to {inv}_{g} (SymGrp (N)) : P ⟶ P$
60	57 59	syl	$⊢ (R \in CRing \land M \in B) \to {inv}_{g} (SymGrp (N)) : P ⟶ P$
61	60	ffvelcdmda	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to {inv}_{g} (SymGrp (N)) (p) \in P$
62	60	feqmptd	$⊢ (R \in CRing \land M \in B) \to {inv}_{g} (SymGrp (N)) = (p \in P ⟼ {inv}_{g} (SymGrp (N)) (p))$
63		eqidd	$⊢ (R \in CRing \land M \in B) \to (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) = (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)))$
64		fveq2	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to (Y \circ S) (q) = (Y \circ S) ({inv}_{g} (SymGrp (N)) (p))$
65		fveq1	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to q (y) = {inv}_{g} (SymGrp (N)) (p) (y)$
66	65	oveq1d	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to q (y) M y = {inv}_{g} (SymGrp (N)) (p) (y) M y$
67	66	mpteq2dv	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to (y \in N ⟼ q (y) M y) = (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y)$
68	67	oveq2d	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to \underset{y \in N}{\sum_{U}} (q (y) M y) = \underset{y \in N}{\sum_{U}} ({inv}_{g} (SymGrp (N)) (p) (y) M y)$
69	64 68	oveq12d	$⊢ q = {inv}_{g} (SymGrp (N)) (p) \to (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y)) = (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, ({inv}_{g} (SymGrp (N)) (p) (y) M y))$
70	61 62 63 69	fmptco	$⊢ (R \in CRing \land M \in B) \to (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) \circ {inv}_{g} (SymGrp (N)) = (p \in P ⟼ (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, ({inv}_{g} (SymGrp (N)) (p) (y) M y)))$
71	19 4 54	symginv	$⊢ p \in P \to {inv}_{g} (SymGrp (N)) (p) = p^{-1}$
72	71	adantl	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to {inv}_{g} (SymGrp (N)) (p) = p^{-1}$
73	72	fveq2d	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) = (Y \circ S) (p^{-1})$
74	12	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to R \in Ring$
75	18	adantr	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to N \in Fin$
76		simpr	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to p \in P$
77	4 5 6	zrhpsgninv	$⊢ (R \in Ring \land N \in Fin \land p \in P) \to (Y \circ S) (p^{-1}) = (Y \circ S) (p)$
78	74 75 76 77	syl3anc	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (Y \circ S) (p^{-1}) = (Y \circ S) (p)$
79	73 78	eqtrd	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) = (Y \circ S) (p)$
80		eqid	$⊢ {Base}_{U} = {Base}_{U}$
81	33	ad2antrr	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to U \in CMnd$
82	39	ad2antrr	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to M : N \times N ⟶ {Base}_{R}$
83	71	ad2antlr	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to {inv}_{g} (SymGrp (N)) (p) = p^{-1}$
84	83	fveq1d	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to {inv}_{g} (SymGrp (N)) (p) (y) = p^{-1} (y)$
85	19 4	symgbasf1o	$⊢ p \in P \to p : N \underset{1-1 onto}{⟶} N$
86	85	adantl	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to p : N \underset{1-1 onto}{⟶} N$
87		f1ocnv	$⊢ p : N \underset{1-1 onto}{⟶} N \to p^{-1} : N \underset{1-1 onto}{⟶} N$
88		f1of	$⊢ p^{-1} : N \underset{1-1 onto}{⟶} N \to p^{-1} : N ⟶ N$
89	86 87 88	3syl	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to p^{-1} : N ⟶ N$
90	89	ffvelcdmda	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to p^{-1} (y) \in N$
91	84 90	eqeltrd	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to {inv}_{g} (SymGrp (N)) (p) (y) \in N$
92		simpr	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to y \in N$
93	82 91 92	fovcdmd	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to {inv}_{g} (SymGrp (N)) (p) (y) M y \in {Base}_{R}$
94	93 32	eleqtrdi	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land y \in N) \to {inv}_{g} (SymGrp (N)) (p) (y) M y \in {Base}_{U}$
95	94	ralrimiva	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to \forall y \in N {inv}_{g} (SymGrp (N)) (p) (y) M y \in {Base}_{U}$
96		eqid	$⊢ (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) = (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y)$
97	80 81 75 95 96 86	gsummptfif1o	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to \underset{y \in N}{\sum_{U}} ({inv}_{g} (SymGrp (N)) (p) (y) M y) = \sum_{U} ((y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) \circ p)$
98		f1of	$⊢ p : N \underset{1-1 onto}{⟶} N \to p : N ⟶ N$
99	86 98	syl	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to p : N ⟶ N$
100	99	ffvelcdmda	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to p (x) \in N$
101	99	feqmptd	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to p = (x \in N ⟼ p (x))$
102		eqidd	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) = (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y)$
103		fveq2	$⊢ y = p (x) \to {inv}_{g} (SymGrp (N)) (p) (y) = {inv}_{g} (SymGrp (N)) (p) (p (x))$
104		id	$⊢ y = p (x) \to y = p (x)$
105	103 104	oveq12d	$⊢ y = p (x) \to {inv}_{g} (SymGrp (N)) (p) (y) M y = {inv}_{g} (SymGrp (N)) (p) (p (x)) M p (x)$
106	100 101 102 105	fmptco	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) \circ p = (x \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (p (x)) M p (x))$
107	71	ad2antlr	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to {inv}_{g} (SymGrp (N)) (p) = p^{-1}$
108	107	fveq1d	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to {inv}_{g} (SymGrp (N)) (p) (p (x)) = p^{-1} (p (x))$
109		f1ocnvfv1	$⊢ (p : N \underset{1-1 onto}{⟶} N \land x \in N) \to p^{-1} (p (x)) = x$
110	86 109	sylan	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to p^{-1} (p (x)) = x$
111	108 110	eqtrd	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to {inv}_{g} (SymGrp (N)) (p) (p (x)) = x$
112	111	oveq1d	$⊢ (((R \in CRing \land M \in B) \land p \in P) \land x \in N) \to {inv}_{g} (SymGrp (N)) (p) (p (x)) M p (x) = x M p (x)$
113	112	mpteq2dva	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (x \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (p (x)) M p (x)) = (x \in N ⟼ x M p (x))$
114	106 113	eqtrd	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) \circ p = (x \in N ⟼ x M p (x))$
115	114	oveq2d	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to \sum_{U} ((y \in N ⟼ {inv}_{g} (SymGrp (N)) (p) (y) M y) \circ p) = \underset{x \in N}{\sum_{U}} (x M p (x))$
116	97 115	eqtrd	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to \underset{y \in N}{\sum_{U}} ({inv}_{g} (SymGrp (N)) (p) (y) M y) = \underset{x \in N}{\sum_{U}} (x M p (x))$
117	79 116	oveq12d	$⊢ ((R \in CRing \land M \in B) \land p \in P) \to (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, ({inv}_{g} (SymGrp (N)) (p) (y) M y)) = (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x)))$
118	117	mpteq2dva	$⊢ (R \in CRing \land M \in B) \to (p \in P ⟼ (Y \circ S) ({inv}_{g} (SymGrp (N)) (p)) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, ({inv}_{g} (SymGrp (N)) (p) (y) M y))) = (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x))))$
119	70 118	eqtrd	$⊢ (R \in CRing \land M \in B) \to (q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) \circ {inv}_{g} (SymGrp (N)) = (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x))))$
120	119	oveq2d	$⊢ (R \in CRing \land M \in B) \to \sum_{R} ((q \in P ⟼ (Y \circ S) (q) \underset{˙}{\cdot} (\underset{y \in N}{\sum_{U}}, (q (y) M y))) \circ {inv}_{g} (SymGrp (N))) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x))))$
121	10 58 120	3eqtrd	$⊢ (R \in CRing \land M \in B) \to D (M) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (x M p (x))))$

Metamath Proof Explorer

Theorem mdetleib2

Proof