This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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