This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → 𝐷 = ∅ )