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 maDet R )
	mdetf.a	|- A = ( N Mat R )
	mdetf.b	|- B = ( Base ` A )
	mdetf.k	|- K = ( Base ` R )
Assertion	mdetcl	|- ( ( R e. CRing /\ M e. B ) -> ( D ` M ) e. K )

Proof

Step	Hyp	Ref	Expression
1		mdetf.d	|- D = ( N maDet R )
2		mdetf.a	|- A = ( N Mat R )
3		mdetf.b	|- B = ( Base ` A )
4		mdetf.k	|- K = ( Base ` R )
5	1 2 3 4	mdetf	|- ( R e. CRing -> D : B --> K )
6	5	ffvelrnda	|- ( ( R e. CRing /\ M e. B ) -> ( D ` M ) e. K )