Metamath Proof Explorer

Theorem lindsdom

Description: A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion lindsdom 
|- ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X ~<_ I )

Proof

Step Hyp Ref Expression
1 drngring 
 |-  ( R e. DivRing -> R e. Ring )
2 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
3 2 frlmlmod 
 |-  ( ( R e. Ring /\ I e. Fin ) -> ( R freeLMod I ) e. LMod )
4 1 3 sylan 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( R freeLMod I ) e. LMod )
5 eqid 
 |-  ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
6 eqid 
 |-  ( LSubSp ` ( R freeLMod I ) ) = ( LSubSp ` ( R freeLMod I ) )
7 5 6 lssmre 
 |-  ( ( R freeLMod I ) e. LMod -> ( LSubSp ` ( R freeLMod I ) ) e. ( Moore ` ( Base ` ( R freeLMod I ) ) ) )
8 4 7 syl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( LSubSp ` ( R freeLMod I ) ) e. ( Moore ` ( Base ` ( R freeLMod I ) ) ) )
9 8 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( LSubSp ` ( R freeLMod I ) ) e. ( Moore ` ( Base ` ( R freeLMod I ) ) ) )
10 eqid 
 |-  ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) = ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) )
11 eqid 
 |-  ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) = ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) )
12 2 frlmsca 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R = ( Scalar ` ( R freeLMod I ) ) )
13 simpl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R e. DivRing )
14 12 13 eqeltrrd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( Scalar ` ( R freeLMod I ) ) e. DivRing )
15 eqid 
 |-  ( Scalar ` ( R freeLMod I ) ) = ( Scalar ` ( R freeLMod I ) )
16 15 islvec 
 |-  ( ( R freeLMod I ) e. LVec <-> ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. DivRing ) )
17 4 14 16 sylanbrc 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( R freeLMod I ) e. LVec )
18 6 10 5 lssacsex 
 |-  ( ( R freeLMod I ) e. LVec -> ( ( LSubSp ` ( R freeLMod I ) ) e. ( ACS ` ( Base ` ( R freeLMod I ) ) ) /\ A. x e. ~P ( Base ` ( R freeLMod I ) ) A. y e. ( Base ` ( R freeLMod I ) ) A. z e. ( ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { z } ) ) ) )
19 17 18 syl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( LSubSp ` ( R freeLMod I ) ) e. ( ACS ` ( Base ` ( R freeLMod I ) ) ) /\ A. x e. ~P ( Base ` ( R freeLMod I ) ) A. y e. ( Base ` ( R freeLMod I ) ) A. z e. ( ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { z } ) ) ) )
20 19 simprd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> A. x e. ~P ( Base ` ( R freeLMod I ) ) A. y e. ( Base ` ( R freeLMod I ) ) A. z e. ( ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { z } ) ) )
21 20 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> A. x e. ~P ( Base ` ( R freeLMod I ) ) A. y e. ( Base ` ( R freeLMod I ) ) A. z e. ( ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { y } ) ) \ ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` x ) ) y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( x u. { z } ) ) )
22 dif0 
 |-  ( ( Base ` ( R freeLMod I ) ) \ (/) ) = ( Base ` ( R freeLMod I ) )
23 22 linds1 
 |-  ( X e. ( LIndS ` ( R freeLMod I ) ) -> X C_ ( ( Base ` ( R freeLMod I ) ) \ (/) ) )
24 23 3ad2ant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( ( Base ` ( R freeLMod I ) ) \ (/) ) )
25 eqid 
 |-  ( R unitVec I ) = ( R unitVec I )
26 25 2 5 uvcff 
 |-  ( ( R e. Ring /\ I e. Fin ) -> ( R unitVec I ) : I --> ( Base ` ( R freeLMod I ) ) )
27 1 26 sylan 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( R unitVec I ) : I --> ( Base ` ( R freeLMod I ) ) )
28 27 frnd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ran ( R unitVec I ) C_ ( Base ` ( R freeLMod I ) ) )
29 28 22 sseqtrrdi 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ran ( R unitVec I ) C_ ( ( Base ` ( R freeLMod I ) ) \ (/) ) )
30 29 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ran ( R unitVec I ) C_ ( ( Base ` ( R freeLMod I ) ) \ (/) ) )
31 5 linds1 
 |-  ( X e. ( LIndS ` ( R freeLMod I ) ) -> X C_ ( Base ` ( R freeLMod I ) ) )
32 31 3ad2ant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( Base ` ( R freeLMod I ) ) )
33 un0 
 |-  ( ran ( R unitVec I ) u. (/) ) = ran ( R unitVec I )
34 33 fveq2i 
 |-  ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( ran ( R unitVec I ) u. (/) ) ) = ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ran ( R unitVec I ) )
35 eqid 
 |-  ( LSpan ` ( R freeLMod I ) ) = ( LSpan ` ( R freeLMod I ) )
36 6 35 10 mrclsp 
 |-  ( ( R freeLMod I ) e. LMod -> ( LSpan ` ( R freeLMod I ) ) = ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) )
37 4 36 syl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( LSpan ` ( R freeLMod I ) ) = ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) )
38 37 fveq1d 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ran ( R unitVec I ) ) = ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ran ( R unitVec I ) ) )
39 eqid 
 |-  ( LBasis ` ( R freeLMod I ) ) = ( LBasis ` ( R freeLMod I ) )
40 2 25 39 frlmlbs 
 |-  ( ( R e. Ring /\ I e. Fin ) -> ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) )
41 1 40 sylan 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) )
42 5 39 35 lbssp 
 |-  ( ran ( R unitVec I ) e. ( LBasis ` ( R freeLMod I ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ran ( R unitVec I ) ) = ( Base ` ( R freeLMod I ) ) )
43 41 42 syl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ran ( R unitVec I ) ) = ( Base ` ( R freeLMod I ) ) )
44 38 43 eqtr3d 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ran ( R unitVec I ) ) = ( Base ` ( R freeLMod I ) ) )
45 34 44 eqtrid 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( ran ( R unitVec I ) u. (/) ) ) = ( Base ` ( R freeLMod I ) ) )
46 45 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( ran ( R unitVec I ) u. (/) ) ) = ( Base ` ( R freeLMod I ) ) )
47 32 46 sseqtrrd 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( ran ( R unitVec I ) u. (/) ) ) )
48 un0 
 |-  ( X u. (/) ) = X
49 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
50 49 adantr 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R e. NzRing )
51 12 50 eqeltrrd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( Scalar ` ( R freeLMod I ) ) e. NzRing )
52 4 51 jca 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) )
53 35 15 lindsind2 
 |-  ( ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) /\ y e. X ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
54 53 3expa 
 |-  ( ( ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. X ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
55 52 54 sylanl1 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. X ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
56 37 fveq1d 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) = ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) )
57 56 eleq2d 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) <-> y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) ) )
58 57 ad2antrr 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. X ) -> ( y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) <-> y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) ) )
59 55 58 mtbid 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. X ) -> -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) )
60 59 ralrimiva 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> A. y e. X -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) )
61 60 3impa 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> A. y e. X -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) )
62 10 11 ismri2 
 |-  ( ( ( LSubSp ` ( R freeLMod I ) ) e. ( Moore ` ( Base ` ( R freeLMod I ) ) ) /\ X C_ ( Base ` ( R freeLMod I ) ) ) -> ( X e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) <-> A. y e. X -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) ) )
63 8 31 62 syl2an 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( X e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) <-> A. y e. X -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) ) )
64 63 3impa 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( X e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) <-> A. y e. X -. y e. ( ( mrCls ` ( LSubSp ` ( R freeLMod I ) ) ) ` ( X \ { y } ) ) ) )
65 61 64 mpbird 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) )
66 48 65 eqeltrid 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( X u. (/) ) e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) )
67 simpr 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> I e. Fin )
68 25 uvcendim 
 |-  ( ( R e. NzRing /\ I e. Fin ) -> I ~~ ran ( R unitVec I ) )
69 49 68 sylan 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> I ~~ ran ( R unitVec I ) )
70 enfi 
 |-  ( I ~~ ran ( R unitVec I ) -> ( I e. Fin <-> ran ( R unitVec I ) e. Fin ) )
71 69 70 syl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( I e. Fin <-> ran ( R unitVec I ) e. Fin ) )
72 67 71 mpbid 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ran ( R unitVec I ) e. Fin )
73 72 olcd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( X e. Fin \/ ran ( R unitVec I ) e. Fin ) )
74 73 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( X e. Fin \/ ran ( R unitVec I ) e. Fin ) )
75 9 10 11 21 24 30 47 66 74 mreexexd 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> E. f e. ~P ran ( R unitVec I ) ( X ~~ f /\ ( f u. (/) ) e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) ) )
76 simpl 
 |-  ( ( X ~~ f /\ ( f u. (/) ) e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) ) -> X ~~ f )
77 ovex 
 |-  ( R unitVec I ) e. _V
78 77 rnex 
 |-  ran ( R unitVec I ) e. _V
79 elpwi 
 |-  ( f e. ~P ran ( R unitVec I ) -> f C_ ran ( R unitVec I ) )
80 ssdomg 
 |-  ( ran ( R unitVec I ) e. _V -> ( f C_ ran ( R unitVec I ) -> f ~<_ ran ( R unitVec I ) ) )
81 78 79 80 mpsyl 
 |-  ( f e. ~P ran ( R unitVec I ) -> f ~<_ ran ( R unitVec I ) )
82 endomtr 
 |-  ( ( X ~~ f /\ f ~<_ ran ( R unitVec I ) ) -> X ~<_ ran ( R unitVec I ) )
83 76 81 82 syl2anr 
 |-  ( ( f e. ~P ran ( R unitVec I ) /\ ( X ~~ f /\ ( f u. (/) ) e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) ) ) -> X ~<_ ran ( R unitVec I ) )
84 83 rexlimiva 
 |-  ( E. f e. ~P ran ( R unitVec I ) ( X ~~ f /\ ( f u. (/) ) e. ( mrInd ` ( LSubSp ` ( R freeLMod I ) ) ) ) -> X ~<_ ran ( R unitVec I ) )
85 75 84 syl 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X ~<_ ran ( R unitVec I ) )
86 69 ensymd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ran ( R unitVec I ) ~~ I )
87 86 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ran ( R unitVec I ) ~~ I )
88 domentr 
 |-  ( ( X ~<_ ran ( R unitVec I ) /\ ran ( R unitVec I ) ~~ I ) -> X ~<_ I )
89 85 87 88 syl2anc 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X ~<_ I )