Metamath Proof Explorer


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 J = LBasis F
Assertion dimval F LVec S J dim F = S

Proof

Step Hyp Ref Expression
1 dimval.1 J = LBasis F
2 elex F LVec F V
3 fveq2 f = F LBasis f = LBasis F
4 3 1 eqtr4di f = F LBasis f = J
5 4 imaeq2d f = F . LBasis f = . J
6 5 unieqd f = F . LBasis f = . J
7 df-dim dim = f V . LBasis f
8 hashf . : V 0 +∞
9 ffun . : V 0 +∞ Fun .
10 1 fvexi J V
11 10 funimaex Fun . . J V
12 8 9 11 mp2b . J V
13 12 uniex . J V
14 6 7 13 fvmpt F V dim F = . J
15 2 14 syl F LVec dim F = . J
16 15 adantr F LVec S J dim F = . J
17 1 lvecdim F LVec S J t J S t
18 17 ad4ant124 F LVec S J x . J t J S t
19 hasheni S t S = t
20 18 19 syl F LVec S J x . J t J S = t
21 20 adantr F LVec S J x . J t J t = x S = t
22 simpr F LVec S J x . J t J t = x t = x
23 21 22 eqtr2d F LVec S J x . J t J t = x x = S
24 8 9 ax-mp Fun .
25 fvelima Fun . x . J t J t = x
26 24 25 mpan x . J t J t = x
27 26 adantl F LVec S J x . J t J t = x
28 23 27 r19.29a F LVec S J x . J x = S
29 28 ralrimiva F LVec S J x . J x = S
30 ne0i S J J
31 30 adantl F LVec S J J
32 ffn . : V 0 +∞ . Fn V
33 8 32 ax-mp . Fn V
34 ssv J V
35 fnimaeq0 . Fn V J V . J = J =
36 33 34 35 mp2an . J = J =
37 36 necon3bii . J J
38 31 37 sylibr F LVec S J . J
39 eqsn . J . J = S x . J x = S
40 38 39 syl F LVec S J . J = S x . J x = S
41 29 40 mpbird F LVec S J . J = S
42 41 unieqd F LVec S J . J = S
43 fvex S V
44 43 unisn S = S
45 44 a1i F LVec S J S = S
46 16 42 45 3eqtrd F LVec S J dim F = S