Metamath Proof Explorer

Theorem dimlssid

Description: If the dimension of a linear subspace L is the dimension of the whole vector space E , then L is the whole space. (Contributed by Thierry Arnoux, 3-Aug-2025)

Ref Expression
Hypotheses dimlssid.b 
|- B = ( Base ` E )
dimlssid.e 
|- ( ph -> E e. LVec )
dimlssid.1 
|- ( ph -> ( dim ` E ) e. NN0 )
dimlssid.l 
|- ( ph -> L e. ( LSubSp ` E ) )
dimlssid.2 
|- ( ph -> ( dim ` ( E |`s L ) ) = ( dim ` E ) )
Assertion dimlssid 
|- ( ph -> L = B )

Proof

Step Hyp Ref Expression
1 dimlssid.b 
 |-  B = ( Base ` E )
2 dimlssid.e 
 |-  ( ph -> E e. LVec )
3 dimlssid.1 
 |-  ( ph -> ( dim ` E ) e. NN0 )
4 dimlssid.l 
 |-  ( ph -> L e. ( LSubSp ` E ) )
5 dimlssid.2 
 |-  ( ph -> ( dim ` ( E |`s L ) ) = ( dim ` E ) )
6 eqid 
 |-  ( E |`s L ) = ( E |`s L )
7 eqid 
 |-  ( LSubSp ` E ) = ( LSubSp ` E )
8 6 7 lsslvec 
 |-  ( ( E e. LVec /\ L e. ( LSubSp ` E ) ) -> ( E |`s L ) e. LVec )
9 2 4 8 syl2anc 
 |-  ( ph -> ( E |`s L ) e. LVec )
10 eqid 
 |-  ( LBasis ` ( E |`s L ) ) = ( LBasis ` ( E |`s L ) )
11 10 lbsex 
 |-  ( ( E |`s L ) e. LVec -> ( LBasis ` ( E |`s L ) ) =/= (/) )
12 9 11 syl 
 |-  ( ph -> ( LBasis ` ( E |`s L ) ) =/= (/) )
13 simplr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> s e. ( LBasis ` E ) )
14 eqid 
 |-  ( LBasis ` E ) = ( LBasis ` E )
15 14 dimval 
 |-  ( ( E e. LVec /\ s e. ( LBasis ` E ) ) -> ( dim ` E ) = ( # ` s ) )
16 2 15 sylan 
 |-  ( ( ph /\ s e. ( LBasis ` E ) ) -> ( dim ` E ) = ( # ` s ) )
17 16 ad4ant13 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( dim ` E ) = ( # ` s ) )
18 3 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( dim ` E ) e. NN0 )
19 17 18 eqeltrrd 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( # ` s ) e. NN0 )
20 hashclb 
 |-  ( s e. ( LBasis ` E ) -> ( s e. Fin <-> ( # ` s ) e. NN0 ) )
21 20 biimpar 
 |-  ( ( s e. ( LBasis ` E ) /\ ( # ` s ) e. NN0 ) -> s e. Fin )
22 13 19 21 syl2anc 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> s e. Fin )
23 simpr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> t C_ s )
24 5 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( dim ` ( E |`s L ) ) = ( dim ` E ) )
25 9 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( E |`s L ) e. LVec )
26 simpllr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> t e. ( LBasis ` ( E |`s L ) ) )
27 10 dimval 
 |-  ( ( ( E |`s L ) e. LVec /\ t e. ( LBasis ` ( E |`s L ) ) ) -> ( dim ` ( E |`s L ) ) = ( # ` t ) )
28 25 26 27 syl2anc 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( dim ` ( E |`s L ) ) = ( # ` t ) )
29 24 28 17 3eqtr3d 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( # ` t ) = ( # ` s ) )
30 22 23 29 phphashrd 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> t = s )
31 30 fveq2d 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( ( LSpan ` E ) ` t ) = ( ( LSpan ` E ) ` s ) )
32 1 7 lssss 
 |-  ( L e. ( LSubSp ` E ) -> L C_ B )
33 6 1 ressbas2 
 |-  ( L C_ B -> L = ( Base ` ( E |`s L ) ) )
34 4 32 33 3syl 
 |-  ( ph -> L = ( Base ` ( E |`s L ) ) )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> L = ( Base ` ( E |`s L ) ) )
36 eqid 
 |-  ( Base ` ( E |`s L ) ) = ( Base ` ( E |`s L ) )
37 eqid 
 |-  ( LSpan ` ( E |`s L ) ) = ( LSpan ` ( E |`s L ) )
38 36 10 37 lbssp 
 |-  ( t e. ( LBasis ` ( E |`s L ) ) -> ( ( LSpan ` ( E |`s L ) ) ` t ) = ( Base ` ( E |`s L ) ) )
39 26 38 syl 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( ( LSpan ` ( E |`s L ) ) ` t ) = ( Base ` ( E |`s L ) ) )
40 2 lveclmodd 
 |-  ( ph -> E e. LMod )
41 40 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> E e. LMod )
42 4 ad3antrrr 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> L e. ( LSubSp ` E ) )
43 36 10 lbsss 
 |-  ( t e. ( LBasis ` ( E |`s L ) ) -> t C_ ( Base ` ( E |`s L ) ) )
44 26 43 syl 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> t C_ ( Base ` ( E |`s L ) ) )
45 44 35 sseqtrrd 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> t C_ L )
46 eqid 
 |-  ( LSpan ` E ) = ( LSpan ` E )
47 6 46 37 7 lsslsp 
 |-  ( ( E e. LMod /\ L e. ( LSubSp ` E ) /\ t C_ L ) -> ( ( LSpan ` ( E |`s L ) ) ` t ) = ( ( LSpan ` E ) ` t ) )
48 41 42 45 47 syl3anc 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( ( LSpan ` ( E |`s L ) ) ` t ) = ( ( LSpan ` E ) ` t ) )
49 35 39 48 3eqtr2rd 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( ( LSpan ` E ) ` t ) = L )
50 1 14 46 lbssp 
 |-  ( s e. ( LBasis ` E ) -> ( ( LSpan ` E ) ` s ) = B )
51 13 50 syl 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> ( ( LSpan ` E ) ` s ) = B )
52 31 49 51 3eqtr3d 
 |-  ( ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ s e. ( LBasis ` E ) ) /\ t C_ s ) -> L = B )
53 2 adantr 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> E e. LVec )
54 43 adantl 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> t C_ ( Base ` ( E |`s L ) ) )
55 34 adantr 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> L = ( Base ` ( E |`s L ) ) )
56 54 55 sseqtrrd 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> t C_ L )
57 4 32 syl 
 |-  ( ph -> L C_ B )
58 57 adantr 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> L C_ B )
59 56 58 sstrd 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> t C_ B )
60 9 lveclmodd 
 |-  ( ph -> ( E |`s L ) e. LMod )
61 60 ad2antrr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> ( E |`s L ) e. LMod )
62 eqid 
 |-  ( Scalar ` E ) = ( Scalar ` E )
63 62 lvecdrng 
 |-  ( E e. LVec -> ( Scalar ` E ) e. DivRing )
64 drngnzr 
 |-  ( ( Scalar ` E ) e. DivRing -> ( Scalar ` E ) e. NzRing )
65 2 63 64 3syl 
 |-  ( ph -> ( Scalar ` E ) e. NzRing )
66 eqid 
 |-  ( 1r ` ( Scalar ` E ) ) = ( 1r ` ( Scalar ` E ) )
67 eqid 
 |-  ( 0g ` ( Scalar ` E ) ) = ( 0g ` ( Scalar ` E ) )
68 66 67 nzrnz 
 |-  ( ( Scalar ` E ) e. NzRing -> ( 1r ` ( Scalar ` E ) ) =/= ( 0g ` ( Scalar ` E ) ) )
69 65 68 syl 
 |-  ( ph -> ( 1r ` ( Scalar ` E ) ) =/= ( 0g ` ( Scalar ` E ) ) )
70 6 62 resssca 
 |-  ( L e. ( LSubSp ` E ) -> ( Scalar ` E ) = ( Scalar ` ( E |`s L ) ) )
71 4 70 syl 
 |-  ( ph -> ( Scalar ` E ) = ( Scalar ` ( E |`s L ) ) )
72 71 fveq2d 
 |-  ( ph -> ( 1r ` ( Scalar ` E ) ) = ( 1r ` ( Scalar ` ( E |`s L ) ) ) )
73 71 fveq2d 
 |-  ( ph -> ( 0g ` ( Scalar ` E ) ) = ( 0g ` ( Scalar ` ( E |`s L ) ) ) )
74 69 72 73 3netr3d 
 |-  ( ph -> ( 1r ` ( Scalar ` ( E |`s L ) ) ) =/= ( 0g ` ( Scalar ` ( E |`s L ) ) ) )
75 74 ad2antrr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> ( 1r ` ( Scalar ` ( E |`s L ) ) ) =/= ( 0g ` ( Scalar ` ( E |`s L ) ) ) )
76 simplr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> t e. ( LBasis ` ( E |`s L ) ) )
77 simpr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> u e. t )
78 eqid 
 |-  ( Scalar ` ( E |`s L ) ) = ( Scalar ` ( E |`s L ) )
79 eqid 
 |-  ( 1r ` ( Scalar ` ( E |`s L ) ) ) = ( 1r ` ( Scalar ` ( E |`s L ) ) )
80 eqid 
 |-  ( 0g ` ( Scalar ` ( E |`s L ) ) ) = ( 0g ` ( Scalar ` ( E |`s L ) ) )
81 10 37 78 79 80 lbsind2 
 |-  ( ( ( ( E |`s L ) e. LMod /\ ( 1r ` ( Scalar ` ( E |`s L ) ) ) =/= ( 0g ` ( Scalar ` ( E |`s L ) ) ) ) /\ t e. ( LBasis ` ( E |`s L ) ) /\ u e. t ) -> -. u e. ( ( LSpan ` ( E |`s L ) ) ` ( t \ { u } ) ) )
82 61 75 76 77 81 syl211anc 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> -. u e. ( ( LSpan ` ( E |`s L ) ) ` ( t \ { u } ) ) )
83 40 ad2antrr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> E e. LMod )
84 4 ad2antrr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> L e. ( LSubSp ` E ) )
85 56 adantr 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> t C_ L )
86 85 ssdifssd 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> ( t \ { u } ) C_ L )
87 6 46 37 7 lsslsp 
 |-  ( ( E e. LMod /\ L e. ( LSubSp ` E ) /\ ( t \ { u } ) C_ L ) -> ( ( LSpan ` ( E |`s L ) ) ` ( t \ { u } ) ) = ( ( LSpan ` E ) ` ( t \ { u } ) ) )
88 83 84 86 87 syl3anc 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> ( ( LSpan ` ( E |`s L ) ) ` ( t \ { u } ) ) = ( ( LSpan ` E ) ` ( t \ { u } ) ) )
89 82 88 neleqtrd 
 |-  ( ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) /\ u e. t ) -> -. u e. ( ( LSpan ` E ) ` ( t \ { u } ) ) )
90 89 ralrimiva 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> A. u e. t -. u e. ( ( LSpan ` E ) ` ( t \ { u } ) ) )
91 14 1 46 lbsext 
 |-  ( ( E e. LVec /\ t C_ B /\ A. u e. t -. u e. ( ( LSpan ` E ) ` ( t \ { u } ) ) ) -> E. s e. ( LBasis ` E ) t C_ s )
92 53 59 90 91 syl3anc 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> E. s e. ( LBasis ` E ) t C_ s )
93 52 92 r19.29a 
 |-  ( ( ph /\ t e. ( LBasis ` ( E |`s L ) ) ) -> L = B )
94 12 93 n0limd 
 |-  ( ph -> L = B )