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 unity element of that ring. (Contributed by AV, 28-Feb-2019)

	Ref	Expression
Assertion	mdet0f1o	|- ( R e. Ring -> ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } )

Proof

Step	Hyp	Ref	Expression
1		mdet0pr	|- ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } )
2		0ex	|- (/) e. _V
3		fvex	|- ( 1r ` R ) e. _V
4	2 3	f1osn	|- { <. (/) , ( 1r ` R ) >. } : { (/) } -1-1-onto-> { ( 1r ` R ) }
5		f1oeq1	|- ( ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } -> ( ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } <-> { <. (/) , ( 1r ` R ) >. } : { (/) } -1-1-onto-> { ( 1r ` R ) } ) )
6	4 5	mpbiri	|- ( ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } -> ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } )
7	1 6	syl	|- ( R e. Ring -> ( (/) maDet R ) : { (/) } -1-1-onto-> { ( 1r ` R ) } )