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	⊢ ( 𝑅 ∈ Ring → ( ( ∅ maDet 𝑅 ) ‘ ∅ ) = ( 1r ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		mdet0pr	⊢ ( 𝑅 ∈ Ring → ( ∅ maDet 𝑅 ) = { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } )
2	1	fveq1d	⊢ ( 𝑅 ∈ Ring → ( ( ∅ maDet 𝑅 ) ‘ ∅ ) = ( { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } ‘ ∅ ) )
3		0ex	⊢ ∅ ∈ V
4		fvex	⊢ ( 1r ‘ 𝑅 ) ∈ V
5	3 4	fvsn	⊢ ( { ⟨ ∅ , ( 1r ‘ 𝑅 ) ⟩ } ‘ ∅ ) = ( 1r ‘ 𝑅 )
6	2 5	eqtrdi	⊢ ( 𝑅 ∈ Ring → ( ( ∅ maDet 𝑅 ) ‘ ∅ ) = ( 1r ‘ 𝑅 ) )