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 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 ) } )