mdet0fv0

Description: The determinant of a 0-dimensional matrix is the 1 element of the underlying ring . (Contributed by AV, 28-Feb-2019)

		Ref	Expression
	Assertion	mdet0fv0	$⊢ R \in Ring \to (\emptyset maDet R) (\emptyset) = 1_{R}$

Step	Hyp	Ref	Expression
1		mdet0pr	$⊢ R \in Ring \to \emptyset maDet R = \{⟨\emptyset, 1_{R}⟩\}$
2	1	fveq1d	$⊢ R \in Ring \to (\emptyset maDet R) (\emptyset) = \{⟨\emptyset, 1_{R}⟩\} (\emptyset)$
3		0ex	$⊢ \emptyset \in V$
4		fvex	$⊢ 1_{R} \in V$
5	3 4	fvsn	$⊢ \{⟨\emptyset, 1_{R}⟩\} (\emptyset) = 1_{R}$
6	2 5	syl6eq	$⊢ R \in Ring \to (\emptyset maDet R) (\emptyset) = 1_{R}$

Metamath Proof Explorer