Theorem nfimdetndef

Description: The determinant is not defined for an infinite matrix. (Contributed by AV, 27-Dec-2018)

	Ref	Expression
Hypothesis	nfimdetndef.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
Assertion	nfimdetndef	⊢ ( 𝑁 ∉ Fin → 𝐷 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		nfimdetndef.d	⊢ 𝐷 = ( 𝑁 maDet 𝑅 )
2		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
3		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
4		eqid	⊢ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
5		eqid	⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
6		eqid	⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
9	1 2 3 4 5 6 7 8	mdetfval	⊢ 𝐷 = ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) )
10		df-nel	⊢ ( 𝑁 ∉ Fin ↔ ¬ 𝑁 ∈ Fin )
11	10	biimpi	⊢ ( 𝑁 ∉ Fin → ¬ 𝑁 ∈ Fin )
12	11	intnanrd	⊢ ( 𝑁 ∉ Fin → ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
13		matbas0	⊢ ( ¬ ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
14	12 13	syl	⊢ ( 𝑁 ∉ Fin → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
15	14	mpteq1d	⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) )
16		mpt0	⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅
17	15 16	eqtrdi	⊢ ( 𝑁 ∉ Fin → ( 𝑚 ∈ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) ↦ ( 𝑅 Σg ( 𝑝 ∈ ( Base ‘ ( SymGrp ‘ 𝑁 ) ) ↦ ( ( ( ( ℤRHom ‘ 𝑅 ) ∘ ( pmSgn ‘ 𝑁 ) ) ‘ 𝑝 ) ( .r ‘ 𝑅 ) ( ( mulGrp ‘ 𝑅 ) Σg ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑝 ‘ 𝑥 ) 𝑚 𝑥 ) ) ) ) ) ) ) = ∅ )
18	9 17	eqtrid	⊢ ( 𝑁 ∉ Fin → 𝐷 = ∅ )