dimvalfi

Description: The dimension of a vector space F is the cardinality of one of its bases. This version of dimval does not depend on the axiom of choice, but it is limited to the case where the base S is finite. (Contributed by Thierry Arnoux, 24-May-2023)

		Ref	Expression
	Hypothesis	dimval.1	$⊢ J = LBasis (F)$
	Assertion	dimvalfi	$⊢ (F \in LVec \land S \in J \land S \in Fin) \to \dim (F) = \|S\|$

Proof

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

Metamath Proof Explorer

Theorem dimvalfi

Proof