mdetpmtr2

Description: The determinant of a matrix with permuted columns 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}$
	mdetpmtr2.e	$⊢ E = (i \in N, j \in N ⟼ i M P (j))$
Assertion	mdetpmtr2	$⊢ ((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		mdetpmtr2.e	$⊢ E = (i \in N, j \in N ⟼ i M P (j))$
9		simpll	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to R \in CRing$
10		simplr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to N \in Fin$
11	1 2	mattposcl	$⊢ M \in B \to tpos M \in B$
12	11	ad2antrl	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to tpos M \in B$
13		simprr	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to P \in G$
14		ovtpos	$⊢ P (j) tpos M i = i M P (j)$
15	14	eqcomi	$⊢ i M P (j) = P (j) tpos M i$
16	15	a1i	$⊢ (i \in N \land j \in N) \to i M P (j) = P (j) tpos M i$
17	16	mpoeq3ia	$⊢ (i \in N, j \in N ⟼ i M P (j)) = (i \in N, j \in N ⟼ P (j) tpos M i)$
18	8 17	eqtri	$⊢ E = (i \in N, j \in N ⟼ P (j) tpos M i)$
19	18	tposmpo	$⊢ tpos E = (j \in N, i \in N ⟼ P (j) tpos M i)$
20	1 2 3 4 5 6 7 19	mdetpmtr1	$⊢ ((R \in CRing \land N \in Fin) \land (tpos M \in B \land P \in G)) \to D (tpos M) = (Z \circ S) (P) \underset{˙}{\cdot} D (tpos E)$
21	9 10 12 13 20	syl22anc	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (tpos M) = (Z \circ S) (P) \underset{˙}{\cdot} D (tpos E)$
22	3 1 2	mdettpos	$⊢ (R \in CRing \land M \in B) \to D (tpos M) = D (M)$
23	22	ad2ant2r	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (tpos M) = D (M)$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25		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$
26	13	3ad2ant1	$⊢ (((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$
27		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$
28		eqid	$⊢ SymGrp (N) = SymGrp (N)$
29	28 4	symgfv	$⊢ (P \in G \land j \in N) \to P (j) \in N$
30	26 27 29	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 (j) \in N$
31		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$
32	1 24 2 25 30 31	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 i M P (j) \in {Base}_{R}$
33	1 24 2 10 9 32	matbas2d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (i \in N, j \in N ⟼ i M P (j)) \in B$
34	8 33	eqeltrid	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to E \in B$
35	3 1 2	mdettpos	$⊢ (R \in CRing \land E \in B) \to D (tpos E) = D (E)$
36	9 34 35	syl2anc	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to D (tpos E) = D (E)$
37	36	oveq2d	$⊢ ((R \in CRing \land N \in Fin) \land (M \in B \land P \in G)) \to (Z \circ S) (P) \underset{˙}{\cdot} D (tpos E) = (Z \circ S) (P) \underset{˙}{\cdot} D (E)$
38	21 23 37	3eqtr3d	$⊢ ((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 mdetpmtr2

Proof