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	ffvelcdmda	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐷 ‘ 𝑀 ) ∈ 𝐾 )