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