Theorem dimval

Description: The dimension of a vector space F is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023)

	Ref	Expression
Hypothesis	dimval.1	$$⊢J=\mathrm{LBasis}\left(F\right)$$
Assertion	dimval	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \dim \left(F\right)=\left|S\right|$$

Proof

Step	Hyp	Ref	Expression
1		dimval.1	$$⊢J=\mathrm{LBasis}\left(F\right)$$
2		elex	$$⊢F\in \mathrm{LVec}\to F\in \mathrm{V}$$
3		fveq2	$$⊢f=F\to \mathrm{LBasis}\left(f\right)=\mathrm{LBasis}\left(F\right)$$
4	3 1	eqtr4di	$$⊢f=F\to \mathrm{LBasis}\left(f\right)=J$$
5	4	imaeq2d	$$⊢f=F\to \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]=\left|.\right|\left[J\right]$$
6	5	unieqd	$$⊢f=F\to \bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]=\bigcup \left|.\right|\left[J\right]$$
7		df-dim	$$⊢\dim =\left(f\in \mathrm{V}⟼\bigcup \left|.\right|\left[\mathrm{LBasis}\left(f\right)\right]\right)$$
8		hashf	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
9		ffun	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \mathrm{Fun}\left|.\right|$$
10	1	fvexi	$$⊢J\in \mathrm{V}$$
11	10	funimaex	$$⊢\mathrm{Fun}\left|.\right|\to \left|.\right|\left[J\right]\in \mathrm{V}$$
12	8 9 11	mp2b	$$⊢\left|.\right|\left[J\right]\in \mathrm{V}$$
13	12	uniex	$$⊢\bigcup \left|.\right|\left[J\right]\in \mathrm{V}$$
14	6 7 13	fvmpt	$$⊢F\in \mathrm{V}\to \dim \left(F\right)=\bigcup \left|.\right|\left[J\right]$$
15	2 14	syl	$$⊢F\in \mathrm{LVec}\to \dim \left(F\right)=\bigcup \left|.\right|\left[J\right]$$
16	15	adantr	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \dim \left(F\right)=\bigcup \left|.\right|\left[J\right]$$
17	1	lvecdim	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\wedge t\in J\right)\to S\approx t$$
18	17	ad4ant124	$$⊢\left(\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\wedge t\in J\right)\to S\approx t$$
19		hasheni	$$⊢S\approx t\to \left|S\right|=\left|t\right|$$
20	18 19	syl	$$⊢\left(\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\wedge t\in J\right)\to \left|S\right|=\left|t\right|$$
21	20	adantr	$$⊢\left(\left(\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\wedge t\in J\right)\wedge \left|t\right|=x\right)\to \left|S\right|=\left|t\right|$$
22		simpr	$$⊢\left(\left(\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\wedge t\in J\right)\wedge \left|t\right|=x\right)\to \left|t\right|=x$$
23	21 22	eqtr2d	$$⊢\left(\left(\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\wedge t\in J\right)\wedge \left|t\right|=x\right)\to x=\left|S\right|$$
24	8 9	ax-mp	$$⊢\mathrm{Fun}\left|.\right|$$
25		fvelima	$$⊢\left(\mathrm{Fun}\left|.\right|\wedge x\in \left|.\right|\left[J\right]\right)\to \exists t\in J\left|t\right|=x$$
26	24 25	mpan	$$⊢x\in \left|.\right|\left[J\right]\to \exists t\in J\left|t\right|=x$$
27	26	adantl	$$⊢\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\to \exists t\in J\left|t\right|=x$$
28	23 27	r19.29a	$$⊢\left(\left(F\in \mathrm{LVec}\wedge S\in J\right)\wedge x\in \left|.\right|\left[J\right]\right)\to x=\left|S\right|$$
29	28	ralrimiva	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \forall x\in \left|.\right|\left[J\right]x=\left|S\right|$$
30		ne0i	$$⊢S\in J\to J\ne \varnothing$$
31	30	adantl	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to J\ne \varnothing$$
32		ffn	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\to \left|.\right|Fn\mathrm{V}$$
33	8 32	ax-mp	$$⊢\left|.\right|Fn\mathrm{V}$$
34		ssv	$$⊢J\subseteq \mathrm{V}$$
35		fnimaeq0	$$⊢\left(\left|.\right|Fn\mathrm{V}\wedge J\subseteq \mathrm{V}\right)\to \left(\left|.\right|\left[J\right]=\varnothing \leftrightarrow J=\varnothing \right)$$
36	33 34 35	mp2an	$$⊢\left|.\right|\left[J\right]=\varnothing \leftrightarrow J=\varnothing$$
37	36	necon3bii	$$⊢\left|.\right|\left[J\right]\ne \varnothing \leftrightarrow J\ne \varnothing$$
38	31 37	sylibr	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \left|.\right|\left[J\right]\ne \varnothing$$
39		eqsn	$$⊢\left|.\right|\left[J\right]\ne \varnothing \to \left(\left|.\right|\left[J\right]=\left\{\left|S\right|\right\}\leftrightarrow \forall x\in \left|.\right|\left[J\right]x=\left|S\right|\right)$$
40	38 39	syl	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \left(\left|.\right|\left[J\right]=\left\{\left|S\right|\right\}\leftrightarrow \forall x\in \left|.\right|\left[J\right]x=\left|S\right|\right)$$
41	29 40	mpbird	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \left|.\right|\left[J\right]=\left\{\left|S\right|\right\}$$
42	41	unieqd	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \bigcup \left|.\right|\left[J\right]=\bigcup \left\{\left|S\right|\right\}$$
43		fvex	$$⊢\left|S\right|\in \mathrm{V}$$
44	43	unisn	$$⊢\bigcup \left\{\left|S\right|\right\}=\left|S\right|$$
45	44	a1i	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \bigcup \left\{\left|S\right|\right\}=\left|S\right|$$
46	16 42 45	3eqtrd	$$⊢\left(F\in \mathrm{LVec}\wedge S\in J\right)\to \dim \left(F\right)=\left|S\right|$$