Theorem matbas0

Description: There is no matrix for a not finite dimension or a proper class as the underlying ring. (Contributed by AV, 28-Dec-2018)

	Ref	Expression
Assertion	matbas0	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-mat	$$⊢\mathrm{Mat}=\left(n\in \mathrm{Fin},r\in \mathrm{V}⟼\left(r\mathrm{freeLMod}\left(n\times n\right)\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},r\mathrm{maMul}⟨n,n,n⟩⟩\right)$$
2	1	mpondm0	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to N\mathrm{Mat}R=\varnothing$$
3	2	fveq2d	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}={\mathrm{Base}}_{\varnothing }$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5	3 4	eqtr4di	$$⊢\neg \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}=\varnothing$$