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∈Jt=x
26 24 25 mpan ⊢x∈.J→∃t∈Jt=x
27 26 adantl ⊢F∈LVec∧S∈J∧x∈.J→∃t∈Jt=x
28 23 27 r19.29a ⊢F∈LVec∧S∈J∧x∈.J→x=S
29 28 ralrimiva ⊢F∈LVec∧S∈J→∀x∈.Jx=S
30 ne0i ⊢S∈J→J≠∅
31 30 adantl ⊢F∈LVec∧S∈J→J≠∅
32 ffn ⊢.:V⟶ℕ0∪+∞→.FnV
33 8 32 ax-mp ⊢.FnV
34 ssv ⊢J⊆V
35 fnimaeq0 ⊢.FnV∧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∈.Jx=S
40 38 39 syl ⊢F∈LVec∧S∈J→.J=S↔∀x∈.Jx=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