mdetpmtr1

Description: The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020)

	Ref	Expression
Hypotheses	mdetpmtr.a	$⊢ A = N Mat R$
	mdetpmtr.b	$⊢ B = {Base}_{A}$
	mdetpmtr.d	$⊢ D = N maDet R$
	mdetpmtr.g	$⊢ G = {Base}_{SymGrp (N)}$
	mdetpmtr.s	$⊢ S = pmSgn (N)$
	mdetpmtr.z	$⊢ Z = ℤRHom (R)$
	mdetpmtr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetpmtr1.e	$⊢ E = (i \in N, j \in N ⟼ P (i) M j)$
Assertion	mdetpmtr1	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (M) = (Z \circ S) (P) \underset{˙}{\cdot} D (E)$

Proof

Step	Hyp	Ref	Expression
1		mdetpmtr.a	$⊢ A = N Mat R$
2		mdetpmtr.b	$⊢ B = {Base}_{A}$
3		mdetpmtr.d	$⊢ D = N maDet R$
4		mdetpmtr.g	$⊢ G = {Base}_{SymGrp (N)}$
5		mdetpmtr.s	$⊢ S = pmSgn (N)$
6		mdetpmtr.z	$⊢ Z = ℤRHom (R)$
7		mdetpmtr.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetpmtr1.e	$⊢ E = (i \in N, j \in N ⟼ P (i) M j)$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10		eqid	$⊢ 0_{R} = 0_{R}$
11		crngring	$⊢ R \in CRing \to R \in Ring$
12	11	ad2antrr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to R \in Ring$
13	4	fvexi	$⊢ G \in V$
14	13	a1i	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to G \in V$
15		simplr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to N \in Fin$
16	5 4	psgndmfi	$⊢ N \in Fin \to S Fn G$
17		fnfun	$⊢ S Fn G \to Fun S$
18	15 16 17	3syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to Fun S$
19		simprr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to P \in G$
20		fndm	$⊢ S Fn G \to dom S = G$
21	15 16 20	3syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to dom S = G$
22	19 21	eleqtrrd	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to P \in dom S$
23		fvco	$⊢ (Fun S \land P \in dom S) \to (Z \circ S) (P) = Z (S (P))$
24	18 22 23	syl2anc	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (Z \circ S) (P) = Z (S (P))$
25	4 5 6	zrhpsgnelbas	$⊢ (R \in Ring \land N \in Fin \land P \in G) \to Z (S (P)) \in {Base}_{R}$
26	12 15 19 25	syl3anc	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to Z (S (P)) \in {Base}_{R}$
27	24 26	eqeltrd	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (Z \circ S) (P) \in {Base}_{R}$
28	12	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to R \in Ring$
29	4 5	cofipsgn	$⊢ (N \in Fin \land p \in G) \to (Z \circ S) (p) = Z (S (p))$
30	15 29	sylan	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (p) = Z (S (p))$
31		simpllr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to N \in Fin$
32		simpr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to p \in G$
33	4 5 6	zrhpsgnelbas	$⊢ (R \in Ring \land N \in Fin \land p \in G) \to Z (S (p)) \in {Base}_{R}$
34	28 31 32 33	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to Z (S (p)) \in {Base}_{R}$
35	30 34	eqeltrd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (p) \in {Base}_{R}$
36		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
37	36 9	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
38	36	crngmgp	$⊢ R \in CRing \to {mulGrp}_{R} \in CMnd$
39	38	ad3antrrr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to {mulGrp}_{R} \in CMnd$
40		eqid	$⊢ SymGrp (N) = SymGrp (N)$
41	40 4	symgfv	$⊢ (p \in G \land x \in N) \to p (x) \in N$
42	41	adantll	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to p (x) \in N$
43		simpr	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to x \in N$
44		simpll	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to R \in CRing$
45		simp1rr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to P \in G$
46		simp2	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to i \in N$
47	40 4	symgfv	$⊢ (P \in G \land i \in N) \to P (i) \in N$
48	45 46 47	syl2anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to P (i) \in N$
49		simp3	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to j \in N$
50		simp1rl	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to M \in B$
51	1 9 2 48 49 50	matecld	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land i \in N \land j \in N) \to P (i) M j \in {Base}_{R}$
52	1 9 2 15 44 51	matbas2d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (i \in N, j \in N ⟼ P (i) M j) \in B$
53	8 52	eqeltrid	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to E \in B$
54	53	ad2antrr	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to E \in B$
55	1 9 2 42 43 54	matecld	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to p (x) E x \in {Base}_{R}$
56	55	ralrimiva	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to \forall x \in N p (x) E x \in {Base}_{R}$
57	37 39 31 56	gsummptcl	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (p (x) E x) \in {Base}_{R}$
58	9 7	ringcl	$⊢ (R \in Ring \land (Z \circ S) (p) \in {Base}_{R} \land \underset{x \in N}{\sum_{{mulGrp}_{R}}} (p (x) E x) \in {Base}_{R}) \to (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) \in {Base}_{R}$
59	28 35 57 58	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) \in {Base}_{R}$
60		eqid	$⊢ (p \in G ⟼ (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))) = (p \in G ⟼ (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))$
61	40 4	symgbasfi	$⊢ N \in Fin \to G \in Fin$
62	15 61	syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to G \in Fin$
63		ovexd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) \in V$
64		fvexd	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to 0_{R} \in V$
65	60 62 63 64	fsuppmptdm	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to {finSupp}_{0_{R}} ((p \in G ⟼ (Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))))$
66	9 10 7 12 14 27 59 65	gsummulc2	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to \underset{p \in G}{\sum_{R}} ((Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))) = (Z \circ S) (P) \underset{˙}{\cdot} (\underset{p \in G}{\sum_{R}}, ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))))$
67		nfcv	$⊢ \underline{Ⅎ} q ((Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x)))$
68		fveq2	$⊢ q = P \circ p \to (Z \circ S) (q) = (Z \circ S) (P \circ p)$
69		fveq1	$⊢ q = P \circ p \to q (x) = (P \circ p) (x)$
70	69	oveq1d	$⊢ q = P \circ p \to q (x) M x = (P \circ p) (x) M x$
71	70	mpteq2dv	$⊢ q = P \circ p \to (x \in N ⟼ q (x) M x) = (x \in N ⟼ (P \circ p) (x) M x)$
72	71	oveq2d	$⊢ q = P \circ p \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (q (x) M x) = \underset{x \in N}{\sum_{{mulGrp}_{R}}} ((P \circ p) (x) M x)$
73	68 72	oveq12d	$⊢ q = P \circ p \to (Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x)) = (Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x))$
74		ringcmn	$⊢ R \in Ring \to R \in CMnd$
75	12 74	syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to R \in CMnd$
76		ssidd	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to {Base}_{R} \subseteq {Base}_{R}$
77	12	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to R \in Ring$
78	4 5	cofipsgn	$⊢ (N \in Fin \land q \in G) \to (Z \circ S) (q) = Z (S (q))$
79	15 78	sylan	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to (Z \circ S) (q) = Z (S (q))$
80		simpllr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to N \in Fin$
81		simpr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to q \in G$
82	4 5 6	zrhpsgnelbas	$⊢ (R \in Ring \land N \in Fin \land q \in G) \to Z (S (q)) \in {Base}_{R}$
83	77 80 81 82	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to Z (S (q)) \in {Base}_{R}$
84	79 83	eqeltrd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to (Z \circ S) (q) \in {Base}_{R}$
85	38	ad3antrrr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to {mulGrp}_{R} \in CMnd$
86	40 4	symgfv	$⊢ (q \in G \land x \in N) \to q (x) \in N$
87	86	adantll	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \land x \in N) \to q (x) \in N$
88		simpr	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \land x \in N) \to x \in N$
89		simprl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to M \in B$
90	89	ad2antrr	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \land x \in N) \to M \in B$
91	1 9 2 87 88 90	matecld	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \land x \in N) \to q (x) M x \in {Base}_{R}$
92	91	ralrimiva	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to \forall x \in N q (x) M x \in {Base}_{R}$
93	37 85 80 92	gsummptcl	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (q (x) M x) \in {Base}_{R}$
94	9 7	ringcl	$⊢ (R \in Ring \land (Z \circ S) (q) \in {Base}_{R} \land \underset{x \in N}{\sum_{{mulGrp}_{R}}} (q (x) M x) \in {Base}_{R}) \to (Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x)) \in {Base}_{R}$
95	77 84 93 94	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to (Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x)) \in {Base}_{R}$
96		eqid	$⊢ +_{SymGrp (N)} = +_{SymGrp (N)}$
97	40 4 96	symgov	$⊢ (P \in G \land p \in G) \to P +_{SymGrp (N)} p = P \circ p$
98	40 4 96	symgcl	$⊢ (P \in G \land p \in G) \to P +_{SymGrp (N)} p \in G$
99	97 98	eqeltrrd	$⊢ (P \in G \land p \in G) \to P \circ p \in G$
100	19 99	sylan	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to P \circ p \in G$
101	19	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to P \in G$
102	4	symgfcoeu	$⊢ (N \in Fin \land P \in G \land q \in G) \to \exists! p \in G q = P \circ p$
103	80 101 81 102	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land q \in G) \to \exists! p \in G q = P \circ p$
104	67 9 10 73 75 62 76 95 100 103	gsummptf1o	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to \underset{q \in G}{\sum_{R}} ((Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x))) = \underset{p \in G}{\sum_{R}} ((Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x)))$
105	3 1 2 4 6 5 7 36	mdetleib	$⊢ M \in B \to D (M) = \underset{q \in G}{\sum_{R}} ((Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x)))$
106	105	ad2antrl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (M) = \underset{q \in G}{\sum_{R}} ((Z \circ S) (q) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (q (x) M x)))$
107	27	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P) \in {Base}_{R}$
108	9 7	ringass	$⊢ (R \in Ring \land ((Z \circ S) (P) \in {Base}_{R} \land (Z \circ S) (p) \in {Base}_{R} \land \underset{x \in N}{\sum_{{mulGrp}_{R}}} (p (x) E x) \in {Base}_{R})) \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) = (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))$
109	28 107 35 57 108	syl13anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) = (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))$
110	24	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P) = Z (S (P))$
111	110 30	oveq12d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (p) = Z (S (P)) \underset{˙}{\cdot} Z (S (p))$
112	4 5	cofipsgn	$⊢ (N \in Fin \land P \circ p \in G) \to (Z \circ S) (P \circ p) = Z (S (P \circ p))$
113	31 100 112	syl2anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P \circ p) = Z (S (P \circ p))$
114	19	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to P \in G$
115	40 5 4	psgnco	$⊢ (N \in Fin \land P \in G \land p \in G) \to S (P \circ p) = S (P) S (p)$
116	31 114 32 115	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to S (P \circ p) = S (P) S (p)$
117	116	fveq2d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to Z (S (P \circ p)) = Z (S (P) S (p))$
118	6	zrhrhm	$⊢ R \in Ring \to Z \in (ℤ_{ring} RingHom R)$
119	12 118	syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to Z \in (ℤ_{ring} RingHom R)$
120	119	adantr	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to Z \in (ℤ_{ring} RingHom R)$
121		1z	$⊢ 1 \in ℤ$
122		neg1z	$⊢ - 1 \in ℤ$
123		prssi	$⊢ (1 \in ℤ \land - 1 \in ℤ) \to \{1, - 1\} \subseteq ℤ$
124	121 122 123	mp2an	$⊢ \{1, - 1\} \subseteq ℤ$
125	4 5	psgnran	$⊢ (N \in Fin \land P \in G) \to S (P) \in \{1, - 1\}$
126	31 114 125	syl2anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to S (P) \in \{1, - 1\}$
127	124 126	sselid	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to S (P) \in ℤ$
128	4 5	psgnran	$⊢ (N \in Fin \land p \in G) \to S (p) \in \{1, - 1\}$
129	15 128	sylan	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to S (p) \in \{1, - 1\}$
130	124 129	sselid	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to S (p) \in ℤ$
131		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
132		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
133	131 132 7	rhmmul	$⊢ (Z \in (ℤ_{ring} RingHom R) \land S (P) \in ℤ \land S (p) \in ℤ) \to Z (S (P) S (p)) = Z (S (P)) \underset{˙}{\cdot} Z (S (p))$
134	120 127 130 133	syl3anc	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to Z (S (P) S (p)) = Z (S (P)) \underset{˙}{\cdot} Z (S (p))$
135	113 117 134	3eqtrrd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to Z (S (P)) \underset{˙}{\cdot} Z (S (p)) = (Z \circ S) (P \circ p)$
136	111 135	eqtrd	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (p) = (Z \circ S) (P \circ p)$
137	8	a1i	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to E = (i \in N, j \in N ⟼ P (i) M j)$
138		simprl	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to i = p (x)$
139	138	fveq2d	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to P (i) = P (p (x))$
140		simpllr	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to p \in G$
141	40 4	symgbasf	$⊢ p \in G \to p : N ⟶ N$
142		ffun	$⊢ p : N ⟶ N \to Fun p$
143	140 141 142	3syl	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to Fun p$
144		simplr	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to x \in N$
145		fdm	$⊢ p : N ⟶ N \to dom p = N$
146	140 141 145	3syl	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to dom p = N$
147	144 146	eleqtrrd	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to x \in dom p$
148		fvco	$⊢ (Fun p \land x \in dom p) \to (P \circ p) (x) = P (p (x))$
149	143 147 148	syl2anc	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to (P \circ p) (x) = P (p (x))$
150	139 149	eqtr4d	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to P (i) = (P \circ p) (x)$
151		simprr	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to j = x$
152	150 151	oveq12d	$⊢ (((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \land (i = p (x) \land j = x)) \to P (i) M j = (P \circ p) (x) M x$
153		ovexd	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to (P \circ p) (x) M x \in V$
154	137 152 42 43 153	ovmpod	$⊢ ((((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \land x \in N) \to p (x) E x = (P \circ p) (x) M x$
155	154	mpteq2dva	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (x \in N ⟼ p (x) E x) = (x \in N ⟼ (P \circ p) (x) M x)$
156	155	oveq2d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to \underset{x \in N}{\sum_{{mulGrp}_{R}}} (p (x) E x) = \underset{x \in N}{\sum_{{mulGrp}_{R}}} ((P \circ p) (x) M x)$
157	136 156	oveq12d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (p)) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)) = (Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x))$
158	109 157	eqtr3d	$⊢ (((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \land p \in G) \to (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))) = (Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x))$
159	158	mpteq2dva	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (p \in G ⟼ (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))) = (p \in G ⟼ (Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x)))$
160	159	oveq2d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to \underset{p \in G}{\sum_{R}} ((Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))) = \underset{p \in G}{\sum_{R}} ((Z \circ S) (P \circ p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, ((P \circ p) (x) M x)))$
161	104 106 160	3eqtr4d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (M) = \underset{p \in G}{\sum_{R}} ((Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))))$
162	3 1 2 4 6 5 7 36	mdetleib	$⊢ E \in B \to D (E) = \underset{p \in G}{\sum_{R}} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))$
163	53 162	syl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (E) = \underset{p \in G}{\sum_{R}} ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x)))$
164	163	oveq2d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (Z \circ S) (P) \underset{˙}{\cdot} D (E) = (Z \circ S) (P) \underset{˙}{\cdot} (\underset{p \in G}{\sum_{R}}, ((Z \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{{mulGrp}_{R}}}, (p (x) E x))))$
165	66 161 164	3eqtr4d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (M) = (Z \circ S) (P) \underset{˙}{\cdot} D (E)$

Metamath Proof Explorer

Theorem mdetpmtr1

Proof