Metamath Proof Explorer

Theorem mdetleib

Description: Full substitution of our determinant definition (also known as Leibniz' Formula, expanding by columns). Proposition 4.6 in Lang p. 514. (Contributed by Stefan O'Rear, 3-Oct-2015) (Revised by SO, 9-Jul-2018)

		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	mdetleib	$⊢ M \in B \to D (M) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M 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		oveq	$⊢ m = M \to p (x) m x = p (x) M x$
10	9	mpteq2dv	$⊢ m = M \to (x \in N ⟼ p (x) m x) = (x \in N ⟼ p (x) M x)$
11	10	oveq2d	$⊢ m = M \to \underset{x \in N}{\sum_{U}} (p (x) m x) = \underset{x \in N}{\sum_{U}} (p (x) M x)$
12	11	oveq2d	$⊢ m = M \to (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x)) = (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M x))$
13	12	mpteq2dv	$⊢ m = M \to (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))) = (p \in P ⟼ (Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M x)))$
14	13	oveq2d	$⊢ m = M \to \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M x)))$
15	1 2 3 4 5 6 7 8	mdetfval	$⊢ D = (m \in B ⟼ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) m x))))$
16		ovex	$⊢ \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M x))) \in V$
17	14 15 16	fvmpt	$⊢ M \in B \to D (M) = \underset{p \in P}{\sum_{R}} ((Y \circ S) (p) \underset{˙}{\cdot} (\underset{x \in N}{\sum_{U}}, (p (x) M x)))$