Theorem mat0dimbas0

Description: The empty set is the one and only matrix of dimension 0, called "the empty matrix". (Contributed by AV, 27-Feb-2019)

	Ref	Expression
Assertion	mat0dimbas0	$$⊢R\in V\to {\mathrm{Base}}_{\left(\varnothing \mathrm{Mat}R\right)}=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0xp	$$⊢\varnothing \times \varnothing =\varnothing$$
2	1	a1i	$$⊢R\in V\to \varnothing \times \varnothing =\varnothing$$
3	2	oveq2d	$$⊢R\in V\to {{\mathrm{Base}}_R}^{\left(\varnothing \times \varnothing \right)}={{\mathrm{Base}}_R}^{\varnothing }$$
4		fvex	$$⊢{\mathrm{Base}}_R\in \mathrm{V}$$
5		map0e	$$⊢{\mathrm{Base}}_R\in \mathrm{V}\to {{\mathrm{Base}}_R}^{\varnothing }=1_{𝑜}$$
6	4 5	mp1i	$$⊢R\in V\to {{\mathrm{Base}}_R}^{\varnothing }=1_{𝑜}$$
7	3 6	eqtrd	$$⊢R\in V\to {{\mathrm{Base}}_R}^{\left(\varnothing \times \varnothing \right)}=1_{𝑜}$$
8		0fi	$$⊢\varnothing \in \mathrm{Fin}$$
9		eqid	$$⊢\varnothing \mathrm{Mat}R=\varnothing \mathrm{Mat}R$$
10		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
11	9 10	matbas2	$$⊢\left(\varnothing \in \mathrm{Fin}\wedge R\in V\right)\to {{\mathrm{Base}}_R}^{\left(\varnothing \times \varnothing \right)}={\mathrm{Base}}_{\left(\varnothing \mathrm{Mat}R\right)}$$
12	8 11	mpan	$$⊢R\in V\to {{\mathrm{Base}}_R}^{\left(\varnothing \times \varnothing \right)}={\mathrm{Base}}_{\left(\varnothing \mathrm{Mat}R\right)}$$
13		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
14	13	a1i	$$⊢R\in V\to 1_{𝑜}=\left\{\varnothing \right\}$$
15	7 12 14	3eqtr3d	$$⊢R\in V\to {\mathrm{Base}}_{\left(\varnothing \mathrm{Mat}R\right)}=\left\{\varnothing \right\}$$