Metamath Proof Explorer

Theorem lindsenlbs

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

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

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> X e. ( LIndS ` ( R freeLMod I ) ) )
2 drngring 
 |-  ( R e. DivRing -> R e. Ring )
3 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
4 3 frlmlmod 
 |-  ( ( R e. Ring /\ I e. Fin ) -> ( R freeLMod I ) e. LMod )
5 2 4 sylan 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( R freeLMod I ) e. LMod )
6 eqid 
 |-  ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
7 6 linds1 
 |-  ( X e. ( LIndS ` ( R freeLMod I ) ) -> X C_ ( Base ` ( R freeLMod I ) ) )
8 eqid 
 |-  ( LSpan ` ( R freeLMod I ) ) = ( LSpan ` ( R freeLMod I ) )
9 6 8 lspssv 
 |-  ( ( ( R freeLMod I ) e. LMod /\ X C_ ( Base ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` X ) C_ ( Base ` ( R freeLMod I ) ) )
10 5 7 9 syl2an 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` X ) C_ ( Base ` ( R freeLMod I ) ) )
11 10 3impa 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` X ) C_ ( Base ` ( R freeLMod I ) ) )
12 11 adantr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> ( ( LSpan ` ( R freeLMod I ) ) ` X ) C_ ( Base ` ( R freeLMod I ) ) )
13 bren2 
 |-  ( X ~~ I <-> ( X ~<_ I /\ -. X ~< I ) )
14 13 simprbi 
 |-  ( X ~~ I -> -. X ~< I )
15 snfi 
 |-  { y } e. Fin
16 simp2 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> I e. Fin )
17 lindsdom 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X ~<_ I )
18 domfi 
 |-  ( ( I e. Fin /\ X ~<_ I ) -> X e. Fin )
19 16 17 18 syl2anc 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X e. Fin )
20 unfi 
 |-  ( ( { y } e. Fin /\ X e. Fin ) -> ( { y } u. X ) e. Fin )
21 15 19 20 sylancr 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( { y } u. X ) e. Fin )
22 21 adantr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> ( { y } u. X ) e. Fin )
23 vex 
 |-  y e. _V
24 23 snss 
 |-  ( y e. X <-> { y } C_ X )
25 6 8 lspssid 
 |-  ( ( ( R freeLMod I ) e. LMod /\ X C_ ( Base ` ( R freeLMod I ) ) ) -> X C_ ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
26 5 7 25 syl2an 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
27 26 3impa 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
28 27 sseld 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( y e. X -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
29 24 28 syl5bir 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( { y } C_ X -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
30 29 con3dimp 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> -. { y } C_ X )
31 nsspssun 
 |-  ( -. { y } C_ X <-> X C. ( { y } u. X ) )
32 30 31 sylib 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> X C. ( { y } u. X ) )
33 php3 
 |-  ( ( ( { y } u. X ) e. Fin /\ X C. ( { y } u. X ) ) -> X ~< ( { y } u. X ) )
34 22 32 33 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> X ~< ( { y } u. X ) )
35 34 adantrl 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> X ~< ( { y } u. X ) )
36 simpl1 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> R e. DivRing )
37 simpl2 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> I e. Fin )
38 snssi 
 |-  ( y e. ( Base ` ( R freeLMod I ) ) -> { y } C_ ( Base ` ( R freeLMod I ) ) )
39 38 adantr 
 |-  ( ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> { y } C_ ( Base ` ( R freeLMod I ) ) )
40 7 3ad2ant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> X C_ ( Base ` ( R freeLMod I ) ) )
41 unss 
 |-  ( ( { y } C_ ( Base ` ( R freeLMod I ) ) /\ X C_ ( Base ` ( R freeLMod I ) ) ) <-> ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) )
42 41 biimpi 
 |-  ( ( { y } C_ ( Base ` ( R freeLMod I ) ) /\ X C_ ( Base ` ( R freeLMod I ) ) ) -> ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) )
43 39 40 42 syl2anr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) )
44 simpr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
45 28 con3dimp 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> -. y e. X )
46 difsn 
 |-  ( -. y e. X -> ( X \ { y } ) = X )
47 45 46 syl 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> ( X \ { y } ) = X )
48 47 fveq2d 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) = ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
49 44 48 neleqtrrd 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
50 49 adantlr 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
51 difsnid 
 |-  ( z e. X -> ( ( X \ { z } ) u. { z } ) = X )
52 51 fveq2d 
 |-  ( z e. X -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) = ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
53 52 eleq2d 
 |-  ( z e. X -> ( y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) <-> y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
54 53 notbid 
 |-  ( z e. X -> ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) <-> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
55 54 biimparc 
 |-  ( ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) /\ z e. X ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) )
56 55 adantll 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) )
57 3 frlmsca 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R = ( Scalar ` ( R freeLMod I ) ) )
58 simpl 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R e. DivRing )
59 57 58 eqeltrrd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( Scalar ` ( R freeLMod I ) ) e. DivRing )
60 eqid 
 |-  ( Scalar ` ( R freeLMod I ) ) = ( Scalar ` ( R freeLMod I ) )
61 60 islvec 
 |-  ( ( R freeLMod I ) e. LVec <-> ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. DivRing ) )
62 5 59 61 sylanbrc 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( R freeLMod I ) e. LVec )
63 62 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( R freeLMod I ) e. LVec )
64 63 ad4antr 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> ( R freeLMod I ) e. LVec )
65 7 ssdifssd 
 |-  ( X e. ( LIndS ` ( R freeLMod I ) ) -> ( X \ { z } ) C_ ( Base ` ( R freeLMod I ) ) )
66 65 3ad2ant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( X \ { z } ) C_ ( Base ` ( R freeLMod I ) ) )
67 66 ad4antr 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> ( X \ { z } ) C_ ( Base ` ( R freeLMod I ) ) )
68 simp-4r 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> y e. ( Base ` ( R freeLMod I ) ) )
69 difundir 
 |-  ( ( { y } u. X ) \ { z } ) = ( ( { y } \ { z } ) u. ( X \ { z } ) )
70 69 equncomi 
 |-  ( ( { y } u. X ) \ { z } ) = ( ( X \ { z } ) u. ( { y } \ { z } ) )
71 elsni 
 |-  ( z e. { y } -> z = y )
72 71 eleq1d 
 |-  ( z e. { y } -> ( z e. X <-> y e. X ) )
73 72 notbid 
 |-  ( z e. { y } -> ( -. z e. X <-> -. y e. X ) )
74 45 73 syl5ibrcom 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> ( z e. { y } -> -. z e. X ) )
75 74 con2d 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> ( z e. X -> -. z e. { y } ) )
76 75 imp 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> -. z e. { y } )
77 difsn 
 |-  ( -. z e. { y } -> ( { y } \ { z } ) = { y } )
78 76 77 syl 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( { y } \ { z } ) = { y } )
79 78 uneq2d 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( ( X \ { z } ) u. ( { y } \ { z } ) ) = ( ( X \ { z } ) u. { y } ) )
80 70 79 syl5eq 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( ( { y } u. X ) \ { z } ) = ( ( X \ { z } ) u. { y } ) )
81 80 fveq2d 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) = ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) )
82 81 eleq2d 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) ) )
83 82 adantllr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) ) )
84 83 biimpa 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) )
85 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
86 85 adantr 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> R e. NzRing )
87 57 86 eqeltrrd 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( Scalar ` ( R freeLMod I ) ) e. NzRing )
88 5 87 jca 
 |-  ( ( R e. DivRing /\ I e. Fin ) -> ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) )
89 88 anim1i 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) )
90 89 3impa 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) )
91 8 60 lindsind2 
 |-  ( ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) /\ z e. X ) -> -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) )
92 91 3expa 
 |-  ( ( ( ( ( R freeLMod I ) e. LMod /\ ( Scalar ` ( R freeLMod I ) ) e. NzRing ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ z e. X ) -> -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) )
93 90 92 sylan 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ z e. X ) -> -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) )
94 93 ad5ant14 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) )
95 84 94 eldifd 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> z e. ( ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) \ ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) ) )
96 eqid 
 |-  ( LSubSp ` ( R freeLMod I ) ) = ( LSubSp ` ( R freeLMod I ) )
97 6 96 8 lspsolv 
 |-  ( ( ( R freeLMod I ) e. LVec /\ ( ( X \ { z } ) C_ ( Base ` ( R freeLMod I ) ) /\ y e. ( Base ` ( R freeLMod I ) ) /\ z e. ( ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { y } ) ) \ ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { z } ) ) ) ) ) -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) )
98 64 67 68 95 97 syl13anc 
 |-  ( ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) /\ z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( X \ { z } ) u. { z } ) ) )
99 56 98 mtand 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) /\ z e. X ) -> -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) )
100 99 ralrimiva 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> A. z e. X -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) )
101 ralunb 
 |-  ( A. z e. ( { y } u. X ) -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( A. z e. { y } -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) /\ A. z e. X -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
102 id 
 |-  ( z = y -> z = y )
103 sneq 
 |-  ( z = y -> { z } = { y } )
104 103 difeq2d 
 |-  ( z = y -> ( ( { y } u. X ) \ { z } ) = ( ( { y } u. X ) \ { y } ) )
105 uncom 
 |-  ( { y } u. X ) = ( X u. { y } )
106 105 difeq1i 
 |-  ( ( { y } u. X ) \ { y } ) = ( ( X u. { y } ) \ { y } )
107 difun2 
 |-  ( ( X u. { y } ) \ { y } ) = ( X \ { y } )
108 106 107 eqtri 
 |-  ( ( { y } u. X ) \ { y } ) = ( X \ { y } )
109 104 108 eqtrdi 
 |-  ( z = y -> ( ( { y } u. X ) \ { z } ) = ( X \ { y } ) )
110 109 fveq2d 
 |-  ( z = y -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) = ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
111 102 110 eleq12d 
 |-  ( z = y -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) ) )
112 111 notbid 
 |-  ( z = y -> ( -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) ) )
113 23 112 ralsn 
 |-  ( A. z e. { y } -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) )
114 113 anbi1i 
 |-  ( ( A. z e. { y } -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) /\ A. z e. X -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) <-> ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) /\ A. z e. X -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
115 101 114 bitri 
 |-  ( A. z e. ( { y } u. X ) -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` ( X \ { y } ) ) /\ A. z e. X -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
116 50 100 115 sylanbrc 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) -> A. z e. ( { y } u. X ) -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) )
117 116 ex 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) -> A. z e. ( { y } u. X ) -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
118 63 ad3antrrr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( R freeLMod I ) e. LVec )
119 eldifsn 
 |-  ( x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) <-> ( x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) /\ x =/= ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) ) )
120 119 biimpi 
 |-  ( x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -> ( x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) /\ x =/= ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) ) )
121 120 adantl 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) /\ x =/= ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) ) )
122 38 7 42 syl2anr 
 |-  ( ( X e. ( LIndS ` ( R freeLMod I ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) )
123 122 3ad2antl3 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) )
124 123 sselda 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) -> z e. ( Base ` ( R freeLMod I ) ) )
125 124 adantr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> z e. ( Base ` ( R freeLMod I ) ) )
126 eqid 
 |-  ( .s ` ( R freeLMod I ) ) = ( .s ` ( R freeLMod I ) )
127 eqid 
 |-  ( Base ` ( Scalar ` ( R freeLMod I ) ) ) = ( Base ` ( Scalar ` ( R freeLMod I ) ) )
128 eqid 
 |-  ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) = ( 0g ` ( Scalar ` ( R freeLMod I ) ) )
129 6 60 126 127 128 8 lspsnvs 
 |-  ( ( ( R freeLMod I ) e. LVec /\ ( x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) /\ x =/= ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) ) /\ z e. ( Base ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` { ( x ( .s ` ( R freeLMod I ) ) z ) } ) = ( ( LSpan ` ( R freeLMod I ) ) ` { z } ) )
130 118 121 125 129 syl3anc 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` { ( x ( .s ` ( R freeLMod I ) ) z ) } ) = ( ( LSpan ` ( R freeLMod I ) ) ` { z } ) )
131 130 sseq1d 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( ( ( LSpan ` ( R freeLMod I ) ) ` { ( x ( .s ` ( R freeLMod I ) ) z ) } ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( ( LSpan ` ( R freeLMod I ) ) ` { z } ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
132 5 3adant3 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) -> ( R freeLMod I ) e. LMod )
133 132 ad3antrrr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( R freeLMod I ) e. LMod )
134 df-3an 
 |-  ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) <-> ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) )
135 122 ssdifssd 
 |-  ( ( X e. ( LIndS ` ( R freeLMod I ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( ( { y } u. X ) \ { z } ) C_ ( Base ` ( R freeLMod I ) ) )
136 6 96 8 lspcl 
 |-  ( ( ( R freeLMod I ) e. LMod /\ ( ( { y } u. X ) \ { z } ) C_ ( Base ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
137 5 135 136 syl2an 
 |-  ( ( ( R e. DivRing /\ I e. Fin ) /\ ( X e. ( LIndS ` ( R freeLMod I ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
138 137 anassrs 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin ) /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
139 134 138 sylanb 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
140 139 ad2antrr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
141 eldifi 
 |-  ( x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -> x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) )
142 141 adantl 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) )
143 6 60 126 127 lmodvscl 
 |-  ( ( ( R freeLMod I ) e. LMod /\ x e. ( Base ` ( Scalar ` ( R freeLMod I ) ) ) /\ z e. ( Base ` ( R freeLMod I ) ) ) -> ( x ( .s ` ( R freeLMod I ) ) z ) e. ( Base ` ( R freeLMod I ) ) )
144 133 142 125 143 syl3anc 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( x ( .s ` ( R freeLMod I ) ) z ) e. ( Base ` ( R freeLMod I ) ) )
145 6 96 8 133 140 144 lspsnel5 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( ( LSpan ` ( R freeLMod I ) ) ` { ( x ( .s ` ( R freeLMod I ) ) z ) } ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
146 132 ad2antrr 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) -> ( R freeLMod I ) e. LMod )
147 139 adantr 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) -> ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) e. ( LSubSp ` ( R freeLMod I ) ) )
148 6 96 8 146 147 124 lspsnel5 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( ( LSpan ` ( R freeLMod I ) ) ` { z } ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
149 148 adantr 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( ( LSpan ` ( R freeLMod I ) ) ` { z } ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
150 131 145 149 3bitr4rd 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
151 150 notbid 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) <-> -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
152 151 biimpd 
 |-  ( ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) /\ x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) -> ( -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) -> -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
153 152 ralrimdva 
 |-  ( ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) /\ z e. ( { y } u. X ) ) -> ( -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) -> A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
154 153 ralimdva 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( A. z e. ( { y } u. X ) -. z e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) -> A. z e. ( { y } u. X ) A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
155 117 154 syld 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ y e. ( Base ` ( R freeLMod I ) ) ) -> ( -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) -> A. z e. ( { y } u. X ) A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
156 155 impr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> A. z e. ( { y } u. X ) A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) )
157 ovex 
 |-  ( R freeLMod I ) e. _V
158 6 126 8 60 127 128 islinds2 
 |-  ( ( R freeLMod I ) e. _V -> ( ( { y } u. X ) e. ( LIndS ` ( R freeLMod I ) ) <-> ( ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) /\ A. z e. ( { y } u. X ) A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) ) )
159 157 158 ax-mp 
 |-  ( ( { y } u. X ) e. ( LIndS ` ( R freeLMod I ) ) <-> ( ( { y } u. X ) C_ ( Base ` ( R freeLMod I ) ) /\ A. z e. ( { y } u. X ) A. x e. ( ( Base ` ( Scalar ` ( R freeLMod I ) ) ) \ { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) -. ( x ( .s ` ( R freeLMod I ) ) z ) e. ( ( LSpan ` ( R freeLMod I ) ) ` ( ( { y } u. X ) \ { z } ) ) ) )
160 43 156 159 sylanbrc 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> ( { y } u. X ) e. ( LIndS ` ( R freeLMod I ) ) )
161 lindsdom 
 |-  ( ( R e. DivRing /\ I e. Fin /\ ( { y } u. X ) e. ( LIndS ` ( R freeLMod I ) ) ) -> ( { y } u. X ) ~<_ I )
162 36 37 160 161 syl3anc 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> ( { y } u. X ) ~<_ I )
163 sdomdomtr 
 |-  ( ( X ~< ( { y } u. X ) /\ ( { y } u. X ) ~<_ I ) -> X ~< I )
164 35 162 163 syl2anc 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) ) -> X ~< I )
165 164 stoic1a 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ -. X ~< I ) -> -. ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
166 14 165 sylan2 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> -. ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
167 iman 
 |-  ( ( y e. ( Base ` ( R freeLMod I ) ) -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) <-> -. ( y e. ( Base ` ( R freeLMod I ) ) /\ -. y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
168 166 167 sylibr 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> ( y e. ( Base ` ( R freeLMod I ) ) -> y e. ( ( LSpan ` ( R freeLMod I ) ) ` X ) ) )
169 168 ssrdv 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> ( Base ` ( R freeLMod I ) ) C_ ( ( LSpan ` ( R freeLMod I ) ) ` X ) )
170 12 169 eqssd 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> ( ( LSpan ` ( R freeLMod I ) ) ` X ) = ( Base ` ( R freeLMod I ) ) )
171 eqid 
 |-  ( LBasis ` ( R freeLMod I ) ) = ( LBasis ` ( R freeLMod I ) )
172 6 171 8 islbs4 
 |-  ( X e. ( LBasis ` ( R freeLMod I ) ) <-> ( X e. ( LIndS ` ( R freeLMod I ) ) /\ ( ( LSpan ` ( R freeLMod I ) ) ` X ) = ( Base ` ( R freeLMod I ) ) ) )
173 1 170 172 sylanbrc 
 |-  ( ( ( R e. DivRing /\ I e. Fin /\ X e. ( LIndS ` ( R freeLMod I ) ) ) /\ X ~~ I ) -> X e. ( LBasis ` ( R freeLMod I ) ) )