Metamath Proof Explorer

Theorem mdet0f1o

Description: The determinant function for 0-dimensional matrices on a given ring is a bijection from the singleton containing the empty set (empty matrix) onto the singleton containing the unit of that ring. (Contributed by AV, 28-Feb-2019)

		Ref	Expression
	Assertion	mdet0f1o	$⊢ R \in Ring \to (\emptyset maDet R) : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\}$

Proof

Step	Hyp	Ref	Expression
1		mdet0pr	$⊢ R \in Ring \to \emptyset maDet R = \{⟨\emptyset, 1_{R}⟩\}$
2		0ex	$⊢ \emptyset \in V$
3		fvex	$⊢ 1_{R} \in V$
4	2 3	f1osn	$⊢ \{⟨\emptyset, 1_{R}⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\}$
5		f1oeq1	$⊢ \emptyset maDet R = \{⟨\emptyset, 1_{R}⟩\} \to ((\emptyset maDet R) : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\} \leftrightarrow \{⟨\emptyset, 1_{R}⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\})$
6	4 5	mpbiri	$⊢ \emptyset maDet R = \{⟨\emptyset, 1_{R}⟩\} \to (\emptyset maDet R) : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\}$
7	1 6	syl	$⊢ R \in Ring \to (\emptyset maDet R) : \{\emptyset\} \underset{1-1 onto}{⟶} \{1_{R}\}$