mdetpmtr12

Description: The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (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}$
	mdetpmtr12.e	$⊢ E = (i \in N, j \in N ⟼ P (i) M Q (j))$
	mdetmptr12.r	$⊢ φ \to R \in CRing$
	mdetmptr12.n	$⊢ φ \to N \in Fin$
	mdetmptr12.m	$⊢ φ \to M \in B$
	mdetmptr12.p	$⊢ φ \to P \in G$
	mdetmptr12.q	$⊢ φ \to Q \in G$
Assertion	mdetpmtr12	$⊢ φ \to D (M) = Z (S (P) S (Q)) \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		mdetpmtr12.e	$⊢ E = (i \in N, j \in N ⟼ P (i) M Q (j))$
9		mdetmptr12.r	$⊢ φ \to R \in CRing$
10		mdetmptr12.n	$⊢ φ \to N \in Fin$
11		mdetmptr12.m	$⊢ φ \to M \in B$
12		mdetmptr12.p	$⊢ φ \to P \in G$
13		mdetmptr12.q	$⊢ φ \to Q \in G$
14		fveq2	$⊢ k = i \to P (k) = P (i)$
15	14	oveq1d	$⊢ k = i \to P (k) M l = P (i) M l$
16		oveq2	$⊢ l = j \to P (i) M l = P (i) M j$
17	15 16	cbvmpov	$⊢ (k \in N, l \in N ⟼ P (k) M l) = (i \in N, j \in N ⟼ P (i) M j)$
18	1 2 3 4 5 6 7 17	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 ((k \in N, l \in N ⟼ P (k) M l))$
19	9 10 11 12 18	syl22anc	$⊢ φ \to D (M) = (Z \circ S) (P) \underset{˙}{\cdot} D ((k \in N, l \in N ⟼ P (k) M l))$
20		eqid	$⊢ {Base}_{R} = {Base}_{R}$
21	12	3ad2ant1	$⊢ (φ \land k \in N \land l \in N) \to P \in G$
22		simp2	$⊢ (φ \land k \in N \land l \in N) \to k \in N$
23		eqid	$⊢ SymGrp (N) = SymGrp (N)$
24	23 4	symgfv	$⊢ (P \in G \land k \in N) \to P (k) \in N$
25	21 22 24	syl2anc	$⊢ (φ \land k \in N \land l \in N) \to P (k) \in N$
26		simp3	$⊢ (φ \land k \in N \land l \in N) \to l \in N$
27	11	3ad2ant1	$⊢ (φ \land k \in N \land l \in N) \to M \in B$
28	1 20 2 25 26 27	matecld	$⊢ (φ \land k \in N \land l \in N) \to P (k) M l \in {Base}_{R}$
29	1 20 2 10 9 28	matbas2d	$⊢ φ \to (k \in N, l \in N ⟼ P (k) M l) \in B$
30		eqid	$⊢ (i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)) = (i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j))$
31	1 2 3 4 5 6 7 30	mdetpmtr2	$⊢ ((R \in CRing \land N \in Fin) \land ((k \in N, l \in N ⟼ P (k) M l) \in B \land Q \in G)) \to D ((k \in N, l \in N ⟼ P (k) M l)) = (Z \circ S) (Q) \underset{˙}{\cdot} D ((i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)))$
32	9 10 29 13 31	syl22anc	$⊢ φ \to D ((k \in N, l \in N ⟼ P (k) M l)) = (Z \circ S) (Q) \underset{˙}{\cdot} D ((i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)))$
33		simp2	$⊢ (φ \land i \in N \land j \in N) \to i \in N$
34	13	3ad2ant1	$⊢ (φ \land i \in N \land j \in N) \to Q \in G$
35		simp3	$⊢ (φ \land i \in N \land j \in N) \to j \in N$
36	23 4	symgfv	$⊢ (Q \in G \land j \in N) \to Q (j) \in N$
37	34 35 36	syl2anc	$⊢ (φ \land i \in N \land j \in N) \to Q (j) \in N$
38		oveq2	$⊢ l = Q (j) \to P (i) M l = P (i) M Q (j)$
39		eqid	$⊢ (k \in N, l \in N ⟼ P (k) M l) = (k \in N, l \in N ⟼ P (k) M l)$
40		ovex	$⊢ P (i) M Q (j) \in V$
41	15 38 39 40	ovmpo	$⊢ (i \in N \land Q (j) \in N) \to i (k \in N, l \in N ⟼ P (k) M l) Q (j) = P (i) M Q (j)$
42	33 37 41	syl2anc	$⊢ (φ \land i \in N \land j \in N) \to i (k \in N, l \in N ⟼ P (k) M l) Q (j) = P (i) M Q (j)$
43	42	mpoeq3dva	$⊢ φ \to (i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)) = (i \in N, j \in N ⟼ P (i) M Q (j))$
44	8 43	eqtr4id	$⊢ φ \to E = (i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j))$
45	44	fveq2d	$⊢ φ \to D (E) = D ((i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)))$
46	45	oveq2d	$⊢ φ \to (Z \circ S) (Q) \underset{˙}{\cdot} D (E) = (Z \circ S) (Q) \underset{˙}{\cdot} D ((i \in N, j \in N ⟼ i (k \in N, l \in N ⟼ P (k) M l) Q (j)))$
47	32 46	eqtr4d	$⊢ φ \to D ((k \in N, l \in N ⟼ P (k) M l)) = (Z \circ S) (Q) \underset{˙}{\cdot} D (E)$
48	47	oveq2d	$⊢ φ \to (Z \circ S) (P) \underset{˙}{\cdot} D ((k \in N, l \in N ⟼ P (k) M l)) = (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (Q) \underset{˙}{\cdot} D (E))$
49		crngring	$⊢ R \in CRing \to R \in Ring$
50	9 49	syl	$⊢ φ \to R \in Ring$
51	4 5 6	zrhcopsgnelbas	$⊢ (R \in Ring \land N \in Fin \land P \in G) \to (Z \circ S) (P) \in {Base}_{R}$
52	50 10 12 51	syl3anc	$⊢ φ \to (Z \circ S) (P) \in {Base}_{R}$
53	4 5 6	zrhcopsgnelbas	$⊢ (R \in Ring \land N \in Fin \land Q \in G) \to (Z \circ S) (Q) \in {Base}_{R}$
54	50 10 13 53	syl3anc	$⊢ φ \to (Z \circ S) (Q) \in {Base}_{R}$
55	12	3ad2ant1	$⊢ (φ \land i \in N \land j \in N) \to P \in G$
56	23 4	symgfv	$⊢ (P \in G \land i \in N) \to P (i) \in N$
57	55 33 56	syl2anc	$⊢ (φ \land i \in N \land j \in N) \to P (i) \in N$
58	11	3ad2ant1	$⊢ (φ \land i \in N \land j \in N) \to M \in B$
59	1 20 2 57 37 58	matecld	$⊢ (φ \land i \in N \land j \in N) \to P (i) M Q (j) \in {Base}_{R}$
60	1 20 2 10 9 59	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ P (i) M Q (j)) \in B$
61	8 60	eqeltrid	$⊢ φ \to E \in B$
62	3 1 2 20	mdetcl	$⊢ (R \in CRing \land E \in B) \to D (E) \in {Base}_{R}$
63	9 61 62	syl2anc	$⊢ φ \to D (E) \in {Base}_{R}$
64	20 7	ringass	$⊢ (R \in Ring \land ((Z \circ S) (P) \in {Base}_{R} \land (Z \circ S) (Q) \in {Base}_{R} \land D (E) \in {Base}_{R})) \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (Q)) \underset{˙}{\cdot} D (E) = (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (Q) \underset{˙}{\cdot} D (E))$
65	50 52 54 63 64	syl13anc	$⊢ φ \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (Q)) \underset{˙}{\cdot} D (E) = (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (Q) \underset{˙}{\cdot} D (E))$
66	4 5	cofipsgn	$⊢ (N \in Fin \land P \in G) \to (Z \circ S) (P) = Z (S (P))$
67	10 12 66	syl2anc	$⊢ φ \to (Z \circ S) (P) = Z (S (P))$
68	4 5	cofipsgn	$⊢ (N \in Fin \land Q \in G) \to (Z \circ S) (Q) = Z (S (Q))$
69	10 13 68	syl2anc	$⊢ φ \to (Z \circ S) (Q) = Z (S (Q))$
70	67 69	oveq12d	$⊢ φ \to (Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (Q) = Z (S (P)) \underset{˙}{\cdot} Z (S (Q))$
71	6	zrhrhm	$⊢ R \in Ring \to Z \in (ℤ_{ring} RingHom R)$
72	50 71	syl	$⊢ φ \to Z \in (ℤ_{ring} RingHom R)$
73		1z	$⊢ 1 \in ℤ$
74		neg1z	$⊢ - 1 \in ℤ$
75		prssi	$⊢ (1 \in ℤ \land - 1 \in ℤ) \to \{1, - 1\} \subseteq ℤ$
76	73 74 75	mp2an	$⊢ \{1, - 1\} \subseteq ℤ$
77	4 5	psgnran	$⊢ (N \in Fin \land P \in G) \to S (P) \in \{1, - 1\}$
78	10 12 77	syl2anc	$⊢ φ \to S (P) \in \{1, - 1\}$
79	76 78	sselid	$⊢ φ \to S (P) \in ℤ$
80	4 5	psgnran	$⊢ (N \in Fin \land Q \in G) \to S (Q) \in \{1, - 1\}$
81	10 13 80	syl2anc	$⊢ φ \to S (Q) \in \{1, - 1\}$
82	76 81	sselid	$⊢ φ \to S (Q) \in ℤ$
83		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
84		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
85	83 84 7	rhmmul	$⊢ (Z \in (ℤ_{ring} RingHom R) \land S (P) \in ℤ \land S (Q) \in ℤ) \to Z (S (P) S (Q)) = Z (S (P)) \underset{˙}{\cdot} Z (S (Q))$
86	72 79 82 85	syl3anc	$⊢ φ \to Z (S (P) S (Q)) = Z (S (P)) \underset{˙}{\cdot} Z (S (Q))$
87	70 86	eqtr4d	$⊢ φ \to (Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (Q) = Z (S (P) S (Q))$
88	87	oveq1d	$⊢ φ \to ((Z \circ S) (P) \underset{˙}{\cdot} (Z \circ S) (Q)) \underset{˙}{\cdot} D (E) = Z (S (P) S (Q)) \underset{˙}{\cdot} D (E)$
89	65 88	eqtr3d	$⊢ φ \to (Z \circ S) (P) \underset{˙}{\cdot} ((Z \circ S) (Q) \underset{˙}{\cdot} D (E)) = Z (S (P) S (Q)) \underset{˙}{\cdot} D (E)$
90	19 48 89	3eqtrd	$⊢ φ \to D (M) = Z (S (P) S (Q)) \underset{˙}{\cdot} D (E)$

Metamath Proof Explorer

Theorem mdetpmtr12

Proof