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 e. LVec /\ S e. J ) -> ( dim ` F ) = ( # ` S ) )

Proof

Step Hyp Ref Expression
1 dimval.1 
 |-  J = ( LBasis ` F )
2 elex 
 |-  ( F e. LVec -> F e. _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 -> U. ( # " ( LBasis ` f ) ) = U. ( # " J ) )
7 df-dim 
 |-  dim = ( f e. _V |-> U. ( # " ( LBasis ` f ) ) )
8 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
9 ffun 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> Fun # )
10 1 fvexi 
 |-  J e. _V
11 10 funimaex 
 |-  ( Fun # -> ( # " J ) e. _V )
12 8 9 11 mp2b 
 |-  ( # " J ) e. _V
13 12 uniex 
 |-  U. ( # " J ) e. _V
14 6 7 13 fvmpt 
 |-  ( F e. _V -> ( dim ` F ) = U. ( # " J ) )
15 2 14 syl 
 |-  ( F e. LVec -> ( dim ` F ) = U. ( # " J ) )
16 15 adantr 
 |-  ( ( F e. LVec /\ S e. J ) -> ( dim ` F ) = U. ( # " J ) )
17 1 lvecdim 
 |-  ( ( F e. LVec /\ S e. J /\ t e. J ) -> S ~~ t )
18 17 ad4ant124 
 |-  ( ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) /\ t e. J ) -> S ~~ t )
19 hasheni 
 |-  ( S ~~ t -> ( # ` S ) = ( # ` t ) )
20 18 19 syl 
 |-  ( ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) /\ t e. J ) -> ( # ` S ) = ( # ` t ) )
21 20 adantr 
 |-  ( ( ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> ( # ` S ) = ( # ` t ) )
22 simpr 
 |-  ( ( ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> ( # ` t ) = x )
23 21 22 eqtr2d 
 |-  ( ( ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> x = ( # ` S ) )
24 8 9 ax-mp 
 |-  Fun #
25 fvelima 
 |-  ( ( Fun # /\ x e. ( # " J ) ) -> E. t e. J ( # ` t ) = x )
26 24 25 mpan 
 |-  ( x e. ( # " J ) -> E. t e. J ( # ` t ) = x )
27 26 adantl 
 |-  ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) -> E. t e. J ( # ` t ) = x )
28 23 27 r19.29a 
 |-  ( ( ( F e. LVec /\ S e. J ) /\ x e. ( # " J ) ) -> x = ( # ` S ) )
29 28 ralrimiva 
 |-  ( ( F e. LVec /\ S e. J ) -> A. x e. ( # " J ) x = ( # ` S ) )
30 ne0i 
 |-  ( S e. J -> J =/= (/) )
31 30 adantl 
 |-  ( ( F e. LVec /\ S e. J ) -> J =/= (/) )
32 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
33 8 32 ax-mp 
 |-  # Fn _V
34 ssv 
 |-  J C_ _V
35 fnimaeq0 
 |-  ( ( # Fn _V /\ J C_ _V ) -> ( ( # " J ) = (/) <-> J = (/) ) )
36 33 34 35 mp2an 
 |-  ( ( # " J ) = (/) <-> J = (/) )
37 36 necon3bii 
 |-  ( ( # " J ) =/= (/) <-> J =/= (/) )
38 31 37 sylibr 
 |-  ( ( F e. LVec /\ S e. J ) -> ( # " J ) =/= (/) )
39 eqsn 
 |-  ( ( # " J ) =/= (/) -> ( ( # " J ) = { ( # ` S ) } <-> A. x e. ( # " J ) x = ( # ` S ) ) )
40 38 39 syl 
 |-  ( ( F e. LVec /\ S e. J ) -> ( ( # " J ) = { ( # ` S ) } <-> A. x e. ( # " J ) x = ( # ` S ) ) )
41 29 40 mpbird 
 |-  ( ( F e. LVec /\ S e. J ) -> ( # " J ) = { ( # ` S ) } )
42 41 unieqd 
 |-  ( ( F e. LVec /\ S e. J ) -> U. ( # " J ) = U. { ( # ` S ) } )
43 fvex 
 |-  ( # ` S ) e. _V
44 43 unisn 
 |-  U. { ( # ` S ) } = ( # ` S )
45 44 a1i 
 |-  ( ( F e. LVec /\ S e. J ) -> U. { ( # ` S ) } = ( # ` S ) )
46 16 42 45 3eqtrd 
 |-  ( ( F e. LVec /\ S e. J ) -> ( dim ` F ) = ( # ` S ) )