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\mathrm{maDet}R$$
Assertion	nfimdetndef	$$⊢N\notin \mathrm{Fin}\to D=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nfimdetndef.d	$$⊢D=N\mathrm{maDet}R$$
2		eqid	$$⊢N\mathrm{Mat}R=N\mathrm{Mat}R$$
3		eqid	$$⊢{\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
4		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
5		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(R\right)=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
6		eqid	$$⊢\mathrm{pmSgn}\left(N\right)=\mathrm{pmSgn}\left(N\right)$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
9	1 2 3 4 5 6 7 8	mdetfval	$$⊢D=\left(m\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}}{{\sum }_R}\left(\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(N\right)\right)\left(p\right){\cdot }_R\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_R}},\left(p\left(x\right)mx\right)\right)\right)\right)$$
10		df-nel	$$⊢N\notin \mathrm{Fin}\leftrightarrow \neg N\in \mathrm{Fin}$$
11	10	biimpi	$$⊢N\notin \mathrm{Fin}\to \neg N\in \mathrm{Fin}$$
12	11	intnanrd	$$⊢N\notin \mathrm{Fin}\to \neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$
13		matbas0	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}=\varnothing$$
14	12 13	syl	$$⊢N\notin \mathrm{Fin}\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}=\varnothing$$
15	14	mpteq1d	$$⊢N\notin \mathrm{Fin}\to \left(m\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}}{{\sum }_R}\left(\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(N\right)\right)\left(p\right){\cdot }_R\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_R}},\left(p\left(x\right)mx\right)\right)\right)\right)=\left(m\in \varnothing ⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}}{{\sum }_R}\left(\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(N\right)\right)\left(p\right){\cdot }_R\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_R}},\left(p\left(x\right)mx\right)\right)\right)\right)$$
16		mpt0	$$⊢\left(m\in \varnothing ⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}}{{\sum }_R}\left(\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(N\right)\right)\left(p\right){\cdot }_R\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_R}},\left(p\left(x\right)mx\right)\right)\right)\right)=\varnothing$$
17	15 16	eqtrdi	$$⊢N\notin \mathrm{Fin}\to \left(m\in {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}⟼\underset{p\in {\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}}{{\sum }_R}\left(\left(\mathrm{\mathbb{Z}RHom}\left(R\right)\circ \mathrm{pmSgn}\left(N\right)\right)\left(p\right){\cdot }_R\left(\underset{x\in N}{{\sum }_{{\mathrm{mulGrp}}_R}},\left(p\left(x\right)mx\right)\right)\right)\right)=\varnothing$$
18	9 17	eqtrid	$$⊢N\notin \mathrm{Fin}\to D=\varnothing$$