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 ) |
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 ) |