Metamath Proof Explorer

Theorem lbslelsp

Description: The size of a basis X of a vector space W is less than the size of a generating set Y . (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses lbslelsp.b 
|- B = ( Base ` W )
lbslelsp.j 
|- J = ( LBasis ` W )
lbslelsp.k 
|- K = ( LSpan ` W )
lbslelsp.w 
|- ( ph -> W e. LVec )
lbslelsp.x 
|- ( ph -> X e. J )
lbslelsp.y 
|- ( ph -> Y C_ B )
lbslelsp.1 
|- ( ph -> ( K ` Y ) = B )
Assertion lbslelsp 
|- ( ph -> ( # ` X ) <_ ( # ` Y ) )

Proof

Step Hyp Ref Expression
1 lbslelsp.b 
 |-  B = ( Base ` W )
2 lbslelsp.j 
 |-  J = ( LBasis ` W )
3 lbslelsp.k 
 |-  K = ( LSpan ` W )
4 lbslelsp.w 
 |-  ( ph -> W e. LVec )
5 lbslelsp.x 
 |-  ( ph -> X e. J )
6 lbslelsp.y 
 |-  ( ph -> Y C_ B )
7 lbslelsp.1 
 |-  ( ph -> ( K ` Y ) = B )
8 4 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> W e. LVec )
9 5 ad3antrrr 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> X e. J )
10 simplr 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> s e. J )
11 2 lvecdim 
 |-  ( ( W e. LVec /\ X e. J /\ s e. J ) -> X ~~ s )
12 8 9 10 11 syl3anc 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> X ~~ s )
13 hasheni 
 |-  ( X ~~ s -> ( # ` X ) = ( # ` s ) )
14 12 13 syl 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> ( # ` X ) = ( # ` s ) )
15 hashss 
 |-  ( ( Y e. Fin /\ s C_ Y ) -> ( # ` s ) <_ ( # ` Y ) )
16 15 ad4ant24 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> ( # ` s ) <_ ( # ` Y ) )
17 14 16 eqbrtrd 
 |-  ( ( ( ( ph /\ Y e. Fin ) /\ s e. J ) /\ s C_ Y ) -> ( # ` X ) <_ ( # ` Y ) )
18 4 adantr 
 |-  ( ( ph /\ Y e. Fin ) -> W e. LVec )
19 simpr 
 |-  ( ( ph /\ Y e. Fin ) -> Y e. Fin )
20 6 adantr 
 |-  ( ( ph /\ Y e. Fin ) -> Y C_ B )
21 7 adantr 
 |-  ( ( ph /\ Y e. Fin ) -> ( K ` Y ) = B )
22 1 2 3 18 19 20 21 exsslsb 
 |-  ( ( ph /\ Y e. Fin ) -> E. s e. J s C_ Y )
23 17 22 r19.29a 
 |-  ( ( ph /\ Y e. Fin ) -> ( # ` X ) <_ ( # ` Y ) )
24 5 adantr 
 |-  ( ( ph /\ -. Y e. Fin ) -> X e. J )
25 hashxrcl 
 |-  ( X e. J -> ( # ` X ) e. RR* )
26 24 25 syl 
 |-  ( ( ph /\ -. Y e. Fin ) -> ( # ` X ) e. RR* )
27 26 pnfged 
 |-  ( ( ph /\ -. Y e. Fin ) -> ( # ` X ) <_ +oo )
28 1 fvexi 
 |-  B e. _V
29 28 a1i 
 |-  ( ph -> B e. _V )
30 29 6 ssexd 
 |-  ( ph -> Y e. _V )
31 hashinf 
 |-  ( ( Y e. _V /\ -. Y e. Fin ) -> ( # ` Y ) = +oo )
32 30 31 sylan 
 |-  ( ( ph /\ -. Y e. Fin ) -> ( # ` Y ) = +oo )
33 27 32 breqtrrd 
 |-  ( ( ph /\ -. Y e. Fin ) -> ( # ` X ) <_ ( # ` Y ) )
34 23 33 pm2.61dan 
 |-  ( ph -> ( # ` X ) <_ ( # ` Y ) )