mdetuni

Description: According to the definition in Weierstrass p. 272, the determinant function is the unique multilinear, alternating and normalized function from the algebra of square matrices of the same dimension over a commutative ring to this ring. So for any multilinear (mdetuni.li and mdetuni.sc), alternating (mdetuni.al) and normalized (mdetuni.no) function D (mdetuni.ff) from the algebra of square matrices (mdetuni.a) to their underlying commutative ring (mdetuni.cr), the function value of this function D for a matrix F (mdetuni.f) is the determinant of this matrix. (Contributed by Stefan O'Rear, 15-Jul-2018) (Revised by Alexander van der Vekens, 8-Feb-2019)

	Ref	Expression
Hypotheses	mdetuni.a	$⊢ A = N Mat R$
	mdetuni.b	$⊢ B = {Base}_{A}$
	mdetuni.k	$⊢ K = {Base}_{R}$
	mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
	mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
	mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
	mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mdetuni.n	$⊢ φ \to N \in Fin$
	mdetuni.r	$⊢ φ \to R \in Ring$
	mdetuni.ff	$⊢ φ \to D : B ⟶ K$
	mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
	mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
	mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
	mdetuni.e	$⊢ E = N maDet R$
	mdetuni.cr	$⊢ φ \to R \in CRing$
	mdetuni.f	$⊢ φ \to F \in B$
	mdetuni.no	$⊢ φ \to D (1_{A}) = \underset{˙}{1}$
Assertion	mdetuni	$⊢ φ \to D (F) = E (F)$

Proof

Step	Hyp	Ref	Expression
1		mdetuni.a	$⊢ A = N Mat R$
2		mdetuni.b	$⊢ B = {Base}_{A}$
3		mdetuni.k	$⊢ K = {Base}_{R}$
4		mdetuni.0g	$⊢ \underset{˙}{0} = 0_{R}$
5		mdetuni.1r	$⊢ \underset{˙}{1} = 1_{R}$
6		mdetuni.pg	$⊢ \underset{˙}{+} = +_{R}$
7		mdetuni.tg	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
8		mdetuni.n	$⊢ φ \to N \in Fin$
9		mdetuni.r	$⊢ φ \to R \in Ring$
10		mdetuni.ff	$⊢ φ \to D : B ⟶ K$
11		mdetuni.al	$⊢ φ \to \forall x \in B \forall y \in N \forall z \in N ((y \neq z \land \forall w \in N y x w = z x w) \to D (x) = \underset{˙}{0})$
12		mdetuni.li	$⊢ φ \to \forall x \in B \forall y \in B \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ({y ↾}_{(\{w\} \times N)}) {\underset{˙}{+}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {y ↾}_{((N ∖ \{w\}) \times N)} \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = D (y) \underset{˙}{+} D (z))$
13		mdetuni.sc	$⊢ φ \to \forall x \in B \forall y \in K \forall z \in B \forall w \in N (({x ↾}_{(\{w\} \times N)} = ((\{w\} \times N) \times \{y\}) {\underset{˙}{\cdot}}_{f} ({z ↾}_{(\{w\} \times N)}) \land {x ↾}_{((N ∖ \{w\}) \times N)} = {z ↾}_{((N ∖ \{w\}) \times N)}) \to D (x) = y \underset{˙}{\cdot} D (z))$
14		mdetuni.e	$⊢ E = N maDet R$
15		mdetuni.cr	$⊢ φ \to R \in CRing$
16		mdetuni.f	$⊢ φ \to F \in B$
17		mdetuni.no	$⊢ φ \to D (1_{A}) = \underset{˙}{1}$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	mdetuni0	$⊢ φ \to D (F) = D (1_{A}) \underset{˙}{\cdot} E (F)$
19	17	oveq1d	$⊢ φ \to D (1_{A}) \underset{˙}{\cdot} E (F) = \underset{˙}{1} \underset{˙}{\cdot} E (F)$
20	14 1 2 3	mdetcl	$⊢ (R \in CRing \land F \in B) \to E (F) \in K$
21	15 16 20	syl2anc	$⊢ φ \to E (F) \in K$
22	3 7 5	ringlidm	$⊢ (R \in Ring \land E (F) \in K) \to \underset{˙}{1} \underset{˙}{\cdot} E (F) = E (F)$
23	9 21 22	syl2anc	$⊢ φ \to \underset{˙}{1} \underset{˙}{\cdot} E (F) = E (F)$
24	18 19 23	3eqtrd	$⊢ φ \to D (F) = E (F)$

Metamath Proof Explorer

Theorem mdetuni

Proof