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	⊢ 𝐽 = ( LBasis ‘ 𝐹 )
Assertion	dimval	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( 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	adantr	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( dim ‘ 𝐹 ) = ∪ ( ♯ “ 𝐽 ) )
17	1	lvecdim	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ∧ 𝑡 ∈ 𝐽 ) → 𝑆 ≈ 𝑡 )
18	17	ad4ant124	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → 𝑆 ≈ 𝑡 )
19		hasheni	⊢ ( 𝑆 ≈ 𝑡 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
20	18 19	syl	⊢ ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
21	20	adantr	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑡 ) )
22		simpr	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → ( ♯ ‘ 𝑡 ) = 𝑥 )
23	21 22	eqtr2d	⊢ ( ( ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) ∧ 𝑡 ∈ 𝐽 ) ∧ ( ♯ ‘ 𝑡 ) = 𝑥 ) → 𝑥 = ( ♯ ‘ 𝑆 ) )
24	8 9	ax-mp	⊢ Fun ♯
25		fvelima	⊢ ( ( Fun ♯ ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
26	24 25	mpan	⊢ ( 𝑥 ∈ ( ♯ “ 𝐽 ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
27	26	adantl	⊢ ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → ∃ 𝑡 ∈ 𝐽 ( ♯ ‘ 𝑡 ) = 𝑥 )
28	23 27	r19.29a	⊢ ( ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ♯ “ 𝐽 ) ) → 𝑥 = ( ♯ ‘ 𝑆 ) )
29	28	ralrimiva	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) )
30		ne0i	⊢ ( 𝑆 ∈ 𝐽 → 𝐽 ≠ ∅ )
31	30	adantl	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → 𝐽 ≠ ∅ )
32		ffn	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
33	8 32	ax-mp	⊢ ♯ Fn V
34		ssv	⊢ 𝐽 ⊆ V
35		fnimaeq0	⊢ ( ( ♯ Fn V ∧ 𝐽 ⊆ V ) → ( ( ♯ “ 𝐽 ) = ∅ ↔ 𝐽 = ∅ ) )
36	33 34 35	mp2an	⊢ ( ( ♯ “ 𝐽 ) = ∅ ↔ 𝐽 = ∅ )
37	36	necon3bii	⊢ ( ( ♯ “ 𝐽 ) ≠ ∅ ↔ 𝐽 ≠ ∅ )
38	31 37	sylibr	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( ♯ “ 𝐽 ) ≠ ∅ )
39		eqsn	⊢ ( ( ♯ “ 𝐽 ) ≠ ∅ → ( ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } ↔ ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) ) )
40	38 39	syl	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } ↔ ∀ 𝑥 ∈ ( ♯ “ 𝐽 ) 𝑥 = ( ♯ ‘ 𝑆 ) ) )
41	29 40	mpbird	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( ♯ “ 𝐽 ) = { ( ♯ ‘ 𝑆 ) } )
42	41	unieqd	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ∪ ( ♯ “ 𝐽 ) = ∪ { ( ♯ ‘ 𝑆 ) } )
43		fvex	⊢ ( ♯ ‘ 𝑆 ) ∈ V
44	43	unisn	⊢ ∪ { ( ♯ ‘ 𝑆 ) } = ( ♯ ‘ 𝑆 )
45	44	a1i	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ∪ { ( ♯ ‘ 𝑆 ) } = ( ♯ ‘ 𝑆 ) )
46	16 42 45	3eqtrd	⊢ ( ( 𝐹 ∈ LVec ∧ 𝑆 ∈ 𝐽 ) → ( dim ‘ 𝐹 ) = ( ♯ ‘ 𝑆 ) )