Theorem 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	⊢ 0 = ( 0g ‘ 𝑉 )
Assertion	lvecdim0	⊢ ( 𝑉 ∈ LVec → ( ( dim ‘ 𝑉 ) = 0 ↔ ( Base ‘ 𝑉 ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		lvecdim0.1	⊢ 0 = ( 0g ‘ 𝑉 )
2	1	lvecdim0i	⊢ ( ( 𝑉 ∈ LVec ∧ ( dim ‘ 𝑉 ) = 0 ) → ( Base ‘ 𝑉 ) = { 0 } )
3		simpl	⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → 𝑉 ∈ LVec )
4		eqid	⊢ ( LBasis ‘ 𝑉 ) = ( LBasis ‘ 𝑉 )
5	4	lbsex	⊢ ( 𝑉 ∈ LVec → ( LBasis ‘ 𝑉 ) ≠ ∅ )
6		n0	⊢ ( ( LBasis ‘ 𝑉 ) ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
7	5 6	sylib	⊢ ( 𝑉 ∈ LVec → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
8	3 7	syl	⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ∃ 𝑏 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
9	1	fvexi	⊢ 0 ∈ V
10	9	snid	⊢ 0 ∈ { 0 }
11		simpr	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 = { 0 } )
12	10 11	eleqtrrid	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 0 ∈ 𝑏 )
13		simplll	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑉 ∈ LVec )
14	4	lbslinds	⊢ ( LBasis ‘ 𝑉 ) ⊆ ( LIndS ‘ 𝑉 )
15		simplr	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
16	14 15	sselid	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → 𝑏 ∈ ( LIndS ‘ 𝑉 ) )
17	1	0nellinds	⊢ ( ( 𝑉 ∈ LVec ∧ 𝑏 ∈ ( LIndS ‘ 𝑉 ) ) → ¬ 0 ∈ 𝑏 )
18	13 16 17	syl2anc	⊢ ( ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) ∧ 𝑏 = { 0 } ) → ¬ 0 ∈ 𝑏 )
19	12 18	pm2.65da	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ¬ 𝑏 = { 0 } )
20		simpr	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ∈ ( LBasis ‘ 𝑉 ) )
21		eqid	⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
22	21 4	lbsss	⊢ ( 𝑏 ∈ ( LBasis ‘ 𝑉 ) → 𝑏 ⊆ ( Base ‘ 𝑉 ) )
23	20 22	syl	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ⊆ ( Base ‘ 𝑉 ) )
24		simplr	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( Base ‘ 𝑉 ) = { 0 } )
25	23 24	sseqtrd	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 ⊆ { 0 } )
26		sssn	⊢ ( 𝑏 ⊆ { 0 } ↔ ( 𝑏 = ∅ ∨ 𝑏 = { 0 } ) )
27	25 26	sylib	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( 𝑏 = ∅ ∨ 𝑏 = { 0 } ) )
28	27	orcomd	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( 𝑏 = { 0 } ∨ 𝑏 = ∅ ) )
29	28	ord	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ( ¬ 𝑏 = { 0 } → 𝑏 = ∅ ) )
30	19 29	mpd	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → 𝑏 = ∅ )
31	30 20	eqeltrrd	⊢ ( ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) ∧ 𝑏 ∈ ( LBasis ‘ 𝑉 ) ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
32	8 31	exlimddv	⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ∅ ∈ ( LBasis ‘ 𝑉 ) )
33	4	dimval	⊢ ( ( 𝑉 ∈ LVec ∧ ∅ ∈ ( LBasis ‘ 𝑉 ) ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ ∅ ) )
34	3 32 33	syl2anc	⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ( dim ‘ 𝑉 ) = ( ♯ ‘ ∅ ) )
35		hash0	⊢ ( ♯ ‘ ∅ ) = 0
36	34 35	eqtrdi	⊢ ( ( 𝑉 ∈ LVec ∧ ( Base ‘ 𝑉 ) = { 0 } ) → ( dim ‘ 𝑉 ) = 0 )
37	2 36	impbida	⊢ ( 𝑉 ∈ LVec → ( ( dim ‘ 𝑉 ) = 0 ↔ ( Base ‘ 𝑉 ) = { 0 } ) )