Theorem 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	⊢ 𝐽 = ( LBasis ‘ 𝐹 )
Assertion	dimvalfi	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		dimval.1	⊢ 𝐽 = ( LBasis ‘ 𝐹 )
2		elex	⊢ ( 𝐹 ∈ LVec → 𝐹 ∈ V )
3		fveq2	⊢ ( 𝑓 = 𝐹 → ( LBasis ‘ 𝑓 ) = ( LBasis ‘ 𝐹 ) )
4	3 1	eqtr4di	⊢ ( 𝑓 = 𝐹 → ( LBasis ‘ 𝑓 ) = 𝐽 )
5	4	imaeq2d	⊢ ( 𝑓 = 𝐹 → ( ♯ “ ( LBasis ‘ 𝑓 ) ) = ( ♯ “ 𝐽 ) )
6	5	unieqd	⊢ ( 𝑓 = 𝐹 → ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) = ∪ ( ♯ “ 𝐽 ) )
7		df-dim	⊢ dim = ( 𝑓 ∈ V ↦ ∪ ( ♯ “ ( LBasis ‘ 𝑓 ) ) )
8		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
9		ffun	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → Fun ♯ )
10	1	fvexi	⊢ 𝐽 ∈ V
11	10	funimaex	⊢ ( Fun ♯ → ( ♯ “ 𝐽 ) ∈ V )
12	8 9 11	mp2b	⊢ ( ♯ “ 𝐽 ) ∈ V
13	12	uniex	⊢ ∪ ( ♯ “ 𝐽 ) ∈ V
14	6 7 13	fvmpt	⊢ ( 𝐹 ∈ V → ( dim ‘ 𝐹 ) = ∪ ( ♯ “ 𝐽 ) )
15	2 14	syl	⊢ ( 𝐹 ∈ LVec → ( dim ‘ 𝐹 ) = ∪ ( ♯ “ 𝐽 ) )
16	15	3ad2ant1	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( dim ‘ 𝐹 ) = ∪ ( ♯ “ 𝐽 ) )
17		simpll1	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝐹 ∈ LVec )
18		simpll2	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝑆 ∈ 𝐽 )
19		simpr	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝑡 ∈ 𝐽 )
20		simpll3	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝑆 ∈ Fin )
21	1 17 18 19 20	lvecdimfi	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝑆 ≈ 𝑡 )
22		hasheni	⊢ ( 𝑆 ≈ 𝑡 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
23	21 22	syl	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
24	23	adantr	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
25		simpr	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → ( ♯ ‘ 𝑡 ) = 𝑥 )
26	24 25	eqtr2d	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → 𝑥 = ( ♯ ‘ 𝑆 ) )
27	8 9	ax-mp	⊢ Fun ♯
28		fvelima	⊢ ( ( Fun ♯ ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
29	27 28	mpan	⊢ ( 𝑥 ∈ ( ♯ “ 𝐽 ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
30	29	adantl	⊢ ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
31	26 30	r19.29a	⊢ ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → 𝑥 = ( ♯ ‘ 𝑆 ) )
32	31	ralrimiva	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) )
33		ne0i	⊢ ( 𝑆 ∈ 𝐽 → 𝐽 ≠ ∅ )
34	33	3ad2ant2	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → 𝐽 ≠ ∅ )
35		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
36	8 35	ax-mp	⊢ ♯ Fn V
37		ssv	⊢ 𝐽 ⊆ V
38		fnimaeq0	⊢ ( ( ♯ Fn V ∧ 𝐽 ⊆ V ) → ( ( ♯ “ 𝐽 ) = ∅ ↔ 𝐽 = ∅ ) )
39	36 37 38	mp2an	⊢ ( ( ♯ “ 𝐽 ) = ∅ ↔ 𝐽 = ∅ )
40	39	necon3bii	⊢ ( ( ♯ “ 𝐽 ) ≠ ∅ ↔ 𝐽 ≠ ∅ )
41	34 40	sylibr	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( ♯ “ 𝐽 ) ≠ ∅ )
42		eqsn	⊢ ( ( ♯ “ 𝐽 ) ≠ ∅ → ( ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } ↔ ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) ) )
43	41 42	syl	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } ↔ ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) ) )
44	32 43	mpbird	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } )
45	44	unieqd	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ∪ ( ♯ “ 𝐽 ) = ∪ { ( ♯ ‘ 𝑆 ) } )
46		fvex	⊢ ( ♯ ‘ 𝑆 ) ∈ V
47	46	unisn	⊢ ∪ { ( ♯ ‘ 𝑆 ) } = ( ♯ ‘ 𝑆 )
48	47	a1i	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ∪ { ( ♯ ‘ 𝑆 ) } = ( ♯ ‘ 𝑆 ) )
49	16 45 48	3eqtrd	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑆 ∈ Fin ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ 𝑆 ) )