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 ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) } )

Proof

Step Hyp Ref Expression
1 mdet0pr ⊢ ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )
2 0ex ⊢ ∅ ∈ V
3 fvex ⊢ ( 1r ‘ 𝑅 ) ∈ V
4 2 3 f1osn ⊢ { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) }
5 f1oeq1 ⊢ ( ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } → ( ( ∅ maDet 𝑅 ) : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) } ↔ { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) } ) )
6 4 5 mpbiri ⊢ ( ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } → ( ∅ maDet 𝑅 ) : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) } )
7 1 6 syl ⊢ ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) : { ∅ } –1-1-onto→ { ( 1r ‘ 𝑅 ) } )