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 𝐷 = ( 𝑁 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 ∧ 𝑀𝐵 ) → ( 𝐷𝑀 ) ∈ 𝐾 )