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 ⊢ D = N maDet R
mdetf.a ⊢ A = N Mat R
mdetf.b ⊢ B = Base A
mdetf.k ⊢ K = Base R
Assertion mdetcl ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ M ∈ K

Proof

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 ∈ CRing → D : B ⟶ K
6 5 ffvelcdmda ⊢ R ∈ CRing ∧ M ∈ B → D ⁡ M ∈ K