Theorem dimcl

Description: Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023)

	Ref	Expression
Assertion	dimcl	$$⊢V\in \mathrm{LVec}\to \dim \left(V\right)\in {\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{LBasis}\left(V\right)=\mathrm{LBasis}\left(V\right)$$
2	1	lbsex	$$⊢V\in \mathrm{LVec}\to \mathrm{LBasis}\left(V\right)\ne \varnothing$$
3		n0	$$⊢\mathrm{LBasis}\left(V\right)\ne \varnothing \leftrightarrow \exists bb\in \mathrm{LBasis}\left(V\right)$$
4	2 3	sylib	$$⊢V\in \mathrm{LVec}\to \exists bb\in \mathrm{LBasis}\left(V\right)$$
5	1	dimval	$$⊢\left(V\in \mathrm{LVec}\wedge b\in \mathrm{LBasis}\left(V\right)\right)\to \dim \left(V\right)=\left|b\right|$$
6		hashxnn0	$$⊢b\in \mathrm{LBasis}\left(V\right)\to \left|b\right|\in {\mathbb{N}}_0^{*}$$
7	6	adantl	$$⊢\left(V\in \mathrm{LVec}\wedge b\in \mathrm{LBasis}\left(V\right)\right)\to \left|b\right|\in {\mathbb{N}}_0^{*}$$
8	5 7	eqeltrd	$$⊢\left(V\in \mathrm{LVec}\wedge b\in \mathrm{LBasis}\left(V\right)\right)\to \dim \left(V\right)\in {\mathbb{N}}_0^{*}$$
9	4 8	exlimddv	$$⊢V\in \mathrm{LVec}\to \dim \left(V\right)\in {\mathbb{N}}_0^{*}$$