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 ⊢ D = N maDet R
Assertion nfimdetndef ⊢ N ∉ Fin → D = ∅

Proof

Step Hyp Ref Expression
1 nfimdetndef.d ⊢ D = N maDet R
2 eqid ⊢ N Mat R = N Mat R
3 eqid ⊢ Base N Mat R = Base N Mat R
4 eqid ⊢ Base SymGrp ⁡ N = Base SymGrp ⁡ N
5 eqid ⊢ ℤRHom ⁡ R = ℤRHom ⁡ R
6 eqid ⊢ pmSgn ⁡ N = pmSgn ⁡ N
7 eqid ⊢ ⋅ R = ⋅ R
8 eqid ⊢ mulGrp R = mulGrp R
9 1 2 3 4 5 6 7 8 mdetfval ⊢ D = m ∈ Base N Mat R ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x m x
10 df-nel ⊢ N ∉ Fin ↔ ¬ N ∈ Fin
11 10 biimpi ⊢ N ∉ Fin → ¬ N ∈ Fin
12 11 intnanrd ⊢ N ∉ Fin → ¬ N ∈ Fin ∧ R ∈ V
13 matbas0 ⊢ ¬ N ∈ Fin ∧ R ∈ V → Base N Mat R = ∅
14 12 13 syl ⊢ N ∉ Fin → Base N Mat R = ∅
15 14 mpteq1d ⊢ N ∉ Fin → m ∈ Base N Mat R ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x m x = m ∈ ∅ ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x m x
16 mpt0 ⊢ m ∈ ∅ ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x m x = ∅
17 15 16 eqtrdi ⊢ N ∉ Fin → m ∈ Base N Mat R ⟼ ∑ R p ∈ Base SymGrp ⁡ N ℤRHom ⁡ R ∘ pmSgn ⁡ N ⁡ p ⋅ R ∑ mulGrp R x ∈ N p ⁡ x m x = ∅
18 9 17 eqtrid ⊢ N ∉ Fin → D = ∅