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	⊢ ( 𝑅 ∈ 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 ‘ 𝑅 ) } )