Metamath Proof Explorer

Theorem 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 e. Ring -> ( ( (/) maDet R ) ` (/) ) = ( 1r ` R ) )

Proof

Step Hyp Ref Expression
1 mdet0pr 
 |-  ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } )
2 1 fveq1d 
 |-  ( R e. Ring -> ( ( (/) maDet R ) ` (/) ) = ( { <. (/) , ( 1r ` R ) >. } ` (/) ) )
3 0ex 
 |-  (/) e. _V
4 fvex 
 |-  ( 1r ` R ) e. _V
5 3 4 fvsn 
 |-  ( { <. (/) , ( 1r ` R ) >. } ` (/) ) = ( 1r ` R )
6 2 5 eqtrdi 
 |-  ( R e. Ring -> ( ( (/) maDet R ) ` (/) ) = ( 1r ` R ) )