Metamath Proof Explorer
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 |
⊢ 𝐷 = ( 𝑁 maDet 𝑅 ) |
|
|
mdetf.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
|
|
mdetf.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
|
|
mdetf.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
|
Assertion |
mdetcl |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) ∈ 𝐾 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
mdetf.d |
⊢ 𝐷 = ( 𝑁 maDet 𝑅 ) |
2 |
|
mdetf.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
3 |
|
mdetf.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
mdetf.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
5 |
1 2 3 4
|
mdetf |
⊢ ( 𝑅 ∈ CRing → 𝐷 : 𝐵 ⟶ 𝐾 ) |
6 |
5
|
ffvelrnda |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) ∈ 𝐾 ) |