Metamath Proof Explorer


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 )