mdet0fv0

Description: The determinant of the empty matrix on a given ring is the unity element of that 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	eqtrdi	$⊢ R \in Ring \to (\emptyset maDet R) (\emptyset) = 1_{R}$

Metamath Proof Explorer