Theorem mdetcl

Description: The determinant evaluates to an element of the base ring. (Contributed by Stefan O'Rear, 9-Sep-2015) (Revised by AV, 7-Feb-2019)

	Ref	Expression
Hypotheses	mdetf.d	$$⊢D=N\mathrm{maDet}R$$
	mdetf.a	$$⊢A=N\mathrm{Mat}R$$
	mdetf.b	$$⊢B={\mathrm{Base}}_A$$
	mdetf.k	$$⊢K={\mathrm{Base}}_R$$
Assertion	mdetcl	$$⊢\left(R\in \mathrm{CRing}\wedge M\in B\right)\to D\left(M\right)\in K$$

Proof

Step	Hyp	Ref	Expression
1		mdetf.d	$$⊢D=N\mathrm{maDet}R$$
2		mdetf.a	$$⊢A=N\mathrm{Mat}R$$
3		mdetf.b	$$⊢B={\mathrm{Base}}_A$$
4		mdetf.k	$$⊢K={\mathrm{Base}}_R$$
5	1 2 3 4	mdetf	$$⊢R\in \mathrm{CRing}\to D:B⟶K$$
6	5	ffvelcdmda	$$⊢\left(R\in \mathrm{CRing}\wedge M\in B\right)\to D\left(M\right)\in K$$