Metamath Proof Explorer

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 
|- J = ( LBasis ` F )
Assertion dimvalfi 
|- ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( 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 3ad2ant1 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( dim ` F ) = U. ( # " J ) )
17 simpll1 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> F e. LVec )
18 simpll2 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> S e. J )
19 simpr 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> t e. J )
20 simpll3 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> S e. Fin )
21 1 17 18 19 20 lvecdimfi 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> S ~~ t )
22 hasheni 
 |-  ( S ~~ t -> ( # ` S ) = ( # ` t ) )
23 21 22 syl 
 |-  ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) -> ( # ` S ) = ( # ` t ) )
24 23 adantr 
 |-  ( ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> ( # ` S ) = ( # ` t ) )
25 simpr 
 |-  ( ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> ( # ` t ) = x )
26 24 25 eqtr2d 
 |-  ( ( ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) /\ t e. J ) /\ ( # ` t ) = x ) -> x = ( # ` S ) )
27 8 9 ax-mp 
 |-  Fun #
28 fvelima 
 |-  ( ( Fun # /\ x e. ( # " J ) ) -> E. t e. J ( # ` t ) = x )
29 27 28 mpan 
 |-  ( x e. ( # " J ) -> E. t e. J ( # ` t ) = x )
30 29 adantl 
 |-  ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) -> E. t e. J ( # ` t ) = x )
31 26 30 r19.29a 
 |-  ( ( ( F e. LVec /\ S e. J /\ S e. Fin ) /\ x e. ( # " J ) ) -> x = ( # ` S ) )
32 31 ralrimiva 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> A. x e. ( # " J ) x = ( # ` S ) )
33 ne0i 
 |-  ( S e. J -> J =/= (/) )
34 33 3ad2ant2 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> J =/= (/) )
35 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
36 8 35 ax-mp 
 |-  # Fn _V
37 ssv 
 |-  J C_ _V
38 fnimaeq0 
 |-  ( ( # Fn _V /\ J C_ _V ) -> ( ( # " J ) = (/) <-> J = (/) ) )
39 36 37 38 mp2an 
 |-  ( ( # " J ) = (/) <-> J = (/) )
40 39 necon3bii 
 |-  ( ( # " J ) =/= (/) <-> J =/= (/) )
41 34 40 sylibr 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( # " J ) =/= (/) )
42 eqsn 
 |-  ( ( # " J ) =/= (/) -> ( ( # " J ) = { ( # ` S ) } <-> A. x e. ( # " J ) x = ( # ` S ) ) )
43 41 42 syl 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( ( # " J ) = { ( # ` S ) } <-> A. x e. ( # " J ) x = ( # ` S ) ) )
44 32 43 mpbird 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( # " J ) = { ( # ` S ) } )
45 44 unieqd 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> U. ( # " J ) = U. { ( # ` S ) } )
46 fvex 
 |-  ( # ` S ) e. _V
47 46 unisn 
 |-  U. { ( # ` S ) } = ( # ` S )
48 47 a1i 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> U. { ( # ` S ) } = ( # ` S ) )
49 16 45 48 3eqtrd 
 |-  ( ( F e. LVec /\ S e. J /\ S e. Fin ) -> ( dim ` F ) = ( # ` S ) )