lvecdim0

Description: A vector space of dimension zero is reduced to its identity element, biconditional version. (Contributed by Thierry Arnoux, 31-Jul-2023)

		Ref	Expression
	Hypothesis	lvecdim0.1	$⊢ \underset{˙}{0} = 0_{V}$
	Assertion	lvecdim0	$⊢ V \in LVec \to (\dim (V) = 0 \leftrightarrow {Base}_{V} = \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		lvecdim0.1	$⊢ \underset{˙}{0} = 0_{V}$
2	1	lvecdim0i	$⊢ (V \in LVec \land \dim (V) = 0) \to {Base}_{V} = \{\underset{˙}{0}\}$
3		simpl	$⊢ (V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \to V \in LVec$
4		eqid	$⊢ LBasis (V) = LBasis (V)$
5	4	lbsex	$⊢ V \in LVec \to LBasis (V) \neq \emptyset$
6		n0	$⊢ LBasis (V) \neq \emptyset \leftrightarrow \exists b b \in LBasis (V)$
7	5 6	sylib	$⊢ V \in LVec \to \exists b b \in LBasis (V)$
8	3 7	syl	$⊢ (V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \to \exists b b \in LBasis (V)$
9	1	fvexi	$⊢ \underset{˙}{0} \in V$
10	9	snid	$⊢ \underset{˙}{0} \in \{\underset{˙}{0}\}$
11		simpr	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to b = \{\underset{˙}{0}\}$
12	10 11	eleqtrrid	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to \underset{˙}{0} \in b$
13		simplll	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to V \in LVec$
14	4	lbslinds	$⊢ LBasis (V) \subseteq LIndS (V)$
15		simplr	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to b \in LBasis (V)$
16	14 15	sseldi	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to b \in LIndS (V)$
17	1	0nellinds	$⊢ (V \in LVec \land b \in LIndS (V)) \to \neg \underset{˙}{0} \in b$
18	13 16 17	syl2anc	$⊢ (((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \land b = \{\underset{˙}{0}\}) \to \neg \underset{˙}{0} \in b$
19	12 18	pm2.65da	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to \neg b = \{\underset{˙}{0}\}$
20		simpr	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to b \in LBasis (V)$
21		eqid	$⊢ {Base}_{V} = {Base}_{V}$
22	21 4	lbsss	$⊢ b \in LBasis (V) \to b \subseteq {Base}_{V}$
23	20 22	syl	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to b \subseteq {Base}_{V}$
24		simplr	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to {Base}_{V} = \{\underset{˙}{0}\}$
25	23 24	sseqtrd	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to b \subseteq \{\underset{˙}{0}\}$
26		sssn	$⊢ b \subseteq \{\underset{˙}{0}\} \leftrightarrow (b = \emptyset \lor b = \{\underset{˙}{0}\})$
27	25 26	sylib	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to (b = \emptyset \lor b = \{\underset{˙}{0}\})$
28	27	orcomd	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to (b = \{\underset{˙}{0}\} \lor b = \emptyset)$
29	28	ord	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to (\neg b = \{\underset{˙}{0}\} \to b = \emptyset)$
30	19 29	mpd	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to b = \emptyset$
31	30 20	eqeltrrd	$⊢ ((V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \land b \in LBasis (V)) \to \emptyset \in LBasis (V)$
32	8 31	exlimddv	$⊢ (V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \to \emptyset \in LBasis (V)$
33	4	dimval	$⊢ (V \in LVec \land \emptyset \in LBasis (V)) \to \dim (V) = \|\emptyset\|$
34	3 32 33	syl2anc	$⊢ (V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \to \dim (V) = \|\emptyset\|$
35		hash0	$⊢ \|\emptyset\| = 0$
36	34 35	syl6eq	$⊢ (V \in LVec \land {Base}_{V} = \{\underset{˙}{0}\}) \to \dim (V) = 0$
37	2 36	impbida	$⊢ V \in LVec \to (\dim (V) = 0 \leftrightarrow {Base}_{V} = \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lvecdim0

Proof