Theorem 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\mathrm{Mat}R$$
	mdetuni.b	$$⊢B={\mathrm{Base}}_A$$
	mdetuni.k	$$⊢K={\mathrm{Base}}_R$$
	mdetuni.0g	$$⊢\underset{\dot{}}{0}=0_R$$
	mdetuni.1r	$$⊢\underset{\dot{}}{1}=1_R$$
	mdetuni.pg	$$⊢\underset{\dot{}}{+}={+}_R$$
	mdetuni.tg	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mdetuni.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mdetuni.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mdetuni.ff	$$⊢\phi \to D:B⟶K$$
	mdetuni.al	$$⊢\phi \to \forall x\in B\forall y\in N\forall z\in N\left(\left(y\ne z\wedge \forall w\in Nyxw=zxw\right)\to D\left(x\right)=\underset{\dot{}}{0}\right)$$
	mdetuni.li	$$⊢\phi \to \forall x\in B\forall y\in B\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left({y\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right){\underset{\dot{}}{+}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={y\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=D\left(y\right)\underset{\dot{}}{+}D\left(z\right)\right)$$
	mdetuni.sc	$$⊢\phi \to \forall x\in B\forall y\in K\forall z\in B\forall w\in N\left(\left({x\upharpoonright }_{\left(\left\{w\right\}\times N\right)}=\left(\left(\left\{w\right\}\times N\right)\times \left\{y\right\}\right){\underset{\dot{}}{·}}_f\left({z\upharpoonright }_{\left(\left\{w\right\}\times N\right)}\right)\wedge {x\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}={z\upharpoonright }_{\left(\left(N\setminus \left\{w\right\}\right)\times N\right)}\right)\to D\left(x\right)=y\underset{\dot{}}{·}D\left(z\right)\right)$$
	mdetuni.e	$$⊢E=N\mathrm{maDet}R$$
	mdetuni.cr	$$⊢\phi \to R\in \mathrm{CRing}$$
	mdetuni.f	$$⊢\phi \to F\in B$$
	mdetuni.no	$$⊢\phi \to D\left(1_A\right)=\underset{\dot{}}{1}$$
Assertion	mdetuni	$$⊢\phi \to D\left(F\right)=E\left(F\right)$$

Proof

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