This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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