Metamath Proof Explorer

Theorem lspsolv

Description: If X is in the span of A u. { Y } but not A , then Y is in the span of A u. { X } . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lspsolv.v 
|- V = ( Base ` W )
lspsolv.s 
|- S = ( LSubSp ` W )
lspsolv.n 
|- N = ( LSpan ` W )
Assertion lspsolv 
|- ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> Y e. ( N ` ( A u. { X } ) ) )

Proof

Step Hyp Ref Expression
1 lspsolv.v 
 |-  V = ( Base ` W )
2 lspsolv.s 
 |-  S = ( LSubSp ` W )
3 lspsolv.n 
 |-  N = ( LSpan ` W )
4 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
5 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
6 eqid 
 |-  ( +g ` W ) = ( +g ` W )
7 eqid 
 |-  ( .s ` W ) = ( .s ` W )
8 eqid 
 |-  { z e. V | E. r e. ( Base ` ( Scalar ` W ) ) ( z ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) } = { z e. V | E. r e. ( Base ` ( Scalar ` W ) ) ( z ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) }
9 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
10 9 adantr 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> W e. LMod )
11 simpr1 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> A C_ V )
12 simpr2 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> Y e. V )
13 simpr3 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) )
14 13 eldifad 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> X e. ( N ` ( A u. { Y } ) ) )
15 1 2 3 4 5 6 7 8 10 11 12 14 lspsolvlem 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> E. r e. ( Base ` ( Scalar ` W ) ) ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) )
16 4 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
17 16 ad2antrr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( Scalar ` W ) e. DivRing )
18 simprl 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> r e. ( Base ` ( Scalar ` W ) ) )
19 10 adantr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> W e. LMod )
20 12 adantr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> Y e. V )
21 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
22 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
23 1 4 7 21 22 lmod0vs 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = ( 0g ` W ) )
24 19 20 23 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) = ( 0g ` W ) )
25 24 oveq2d 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) = ( X ( +g ` W ) ( 0g ` W ) ) )
26 11 adantr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> A C_ V )
27 20 snssd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> { Y } C_ V )
28 26 27 unssd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( A u. { Y } ) C_ V )
29 1 3 lspssv 
 |-  ( ( W e. LMod /\ ( A u. { Y } ) C_ V ) -> ( N ` ( A u. { Y } ) ) C_ V )
30 19 28 29 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( N ` ( A u. { Y } ) ) C_ V )
31 30 ssdifssd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) C_ V )
32 13 adantr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) )
33 31 32 sseldd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> X e. V )
34 1 6 22 lmod0vrid 
 |-  ( ( W e. LMod /\ X e. V ) -> ( X ( +g ` W ) ( 0g ` W ) ) = X )
35 19 33 34 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( 0g ` W ) ) = X )
36 25 35 eqtrd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) = X )
37 36 32 eqeltrd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) )
38 37 eldifbd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> -. ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) e. ( N ` A ) )
39 simprr 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) )
40 oveq1 
 |-  ( r = ( 0g ` ( Scalar ` W ) ) -> ( r ( .s ` W ) Y ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) )
41 40 oveq2d 
 |-  ( r = ( 0g ` ( Scalar ` W ) ) -> ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) = ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) )
42 41 eleq1d 
 |-  ( r = ( 0g ` ( Scalar ` W ) ) -> ( ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) <-> ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) e. ( N ` A ) ) )
43 39 42 syl5ibcom 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( r = ( 0g ` ( Scalar ` W ) ) -> ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) e. ( N ` A ) ) )
44 43 necon3bd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( -. ( X ( +g ` W ) ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) Y ) ) e. ( N ` A ) -> r =/= ( 0g ` ( Scalar ` W ) ) ) )
45 38 44 mpd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> r =/= ( 0g ` ( Scalar ` W ) ) )
46 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
47 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
48 eqid 
 |-  ( invr ` ( Scalar ` W ) ) = ( invr ` ( Scalar ` W ) )
49 5 21 46 47 48 drnginvrl 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ r e. ( Base ` ( Scalar ` W ) ) /\ r =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .r ` ( Scalar ` W ) ) r ) = ( 1r ` ( Scalar ` W ) ) )
50 17 18 45 49 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .r ` ( Scalar ` W ) ) r ) = ( 1r ` ( Scalar ` W ) ) )
51 50 oveq1d 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) Y ) = ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) )
52 5 21 48 drnginvrcl 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ r e. ( Base ` ( Scalar ` W ) ) /\ r =/= ( 0g ` ( Scalar ` W ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` r ) e. ( Base ` ( Scalar ` W ) ) )
53 17 18 45 52 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( invr ` ( Scalar ` W ) ) ` r ) e. ( Base ` ( Scalar ` W ) ) )
54 1 4 7 5 46 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( ( invr ` ( Scalar ` W ) ) ` r ) e. ( Base ` ( Scalar ` W ) ) /\ r e. ( Base ` ( Scalar ` W ) ) /\ Y e. V ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) Y ) = ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .s ` W ) ( r ( .s ` W ) Y ) ) )
55 19 53 18 20 54 syl13anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .r ` ( Scalar ` W ) ) r ) ( .s ` W ) Y ) = ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .s ` W ) ( r ( .s ` W ) Y ) ) )
56 1 4 7 47 lmodvs1 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) = Y )
57 19 20 56 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( 1r ` ( Scalar ` W ) ) ( .s ` W ) Y ) = Y )
58 51 55 57 3eqtr3d 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .s ` W ) ( r ( .s ` W ) Y ) ) = Y )
59 33 snssd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> { X } C_ V )
60 26 59 unssd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( A u. { X } ) C_ V )
61 1 2 3 lspcl 
 |-  ( ( W e. LMod /\ ( A u. { X } ) C_ V ) -> ( N ` ( A u. { X } ) ) e. S )
62 19 60 61 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( N ` ( A u. { X } ) ) e. S )
63 1 4 7 5 lmodvscl 
 |-  ( ( W e. LMod /\ r e. ( Base ` ( Scalar ` W ) ) /\ Y e. V ) -> ( r ( .s ` W ) Y ) e. V )
64 19 18 20 63 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( r ( .s ` W ) Y ) e. V )
65 eqid 
 |-  ( -g ` W ) = ( -g ` W )
66 1 6 65 lmodvpncan 
 |-  ( ( W e. LMod /\ ( r ( .s ` W ) Y ) e. V /\ X e. V ) -> ( ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) ( -g ` W ) X ) = ( r ( .s ` W ) Y ) )
67 19 64 33 66 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) ( -g ` W ) X ) = ( r ( .s ` W ) Y ) )
68 1 6 lmodcom 
 |-  ( ( W e. LMod /\ ( r ( .s ` W ) Y ) e. V /\ X e. V ) -> ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) = ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) )
69 19 64 33 68 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) = ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) )
70 ssun1 
 |-  A C_ ( A u. { X } )
71 70 a1i 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> A C_ ( A u. { X } ) )
72 1 3 lspss 
 |-  ( ( W e. LMod /\ ( A u. { X } ) C_ V /\ A C_ ( A u. { X } ) ) -> ( N ` A ) C_ ( N ` ( A u. { X } ) ) )
73 19 60 71 72 syl3anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( N ` A ) C_ ( N ` ( A u. { X } ) ) )
74 73 39 sseldd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` ( A u. { X } ) ) )
75 69 74 eqeltrd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) e. ( N ` ( A u. { X } ) ) )
76 1 3 lspssid 
 |-  ( ( W e. LMod /\ ( A u. { X } ) C_ V ) -> ( A u. { X } ) C_ ( N ` ( A u. { X } ) ) )
77 19 60 76 syl2anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( A u. { X } ) C_ ( N ` ( A u. { X } ) ) )
78 snidg 
 |-  ( X e. V -> X e. { X } )
79 elun2 
 |-  ( X e. { X } -> X e. ( A u. { X } ) )
80 33 78 79 3syl 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> X e. ( A u. { X } ) )
81 77 80 sseldd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> X e. ( N ` ( A u. { X } ) ) )
82 65 2 lssvsubcl 
 |-  ( ( ( W e. LMod /\ ( N ` ( A u. { X } ) ) e. S ) /\ ( ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) e. ( N ` ( A u. { X } ) ) /\ X e. ( N ` ( A u. { X } ) ) ) ) -> ( ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) ( -g ` W ) X ) e. ( N ` ( A u. { X } ) ) )
83 19 62 75 81 82 syl22anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( r ( .s ` W ) Y ) ( +g ` W ) X ) ( -g ` W ) X ) e. ( N ` ( A u. { X } ) ) )
84 67 83 eqeltrrd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( r ( .s ` W ) Y ) e. ( N ` ( A u. { X } ) ) )
85 4 7 5 2 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` ( A u. { X } ) ) e. S ) /\ ( ( ( invr ` ( Scalar ` W ) ) ` r ) e. ( Base ` ( Scalar ` W ) ) /\ ( r ( .s ` W ) Y ) e. ( N ` ( A u. { X } ) ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .s ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` ( A u. { X } ) ) )
86 19 62 53 84 85 syl22anc 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> ( ( ( invr ` ( Scalar ` W ) ) ` r ) ( .s ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` ( A u. { X } ) ) )
87 58 86 eqeltrrd 
 |-  ( ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) /\ ( r e. ( Base ` ( Scalar ` W ) ) /\ ( X ( +g ` W ) ( r ( .s ` W ) Y ) ) e. ( N ` A ) ) ) -> Y e. ( N ` ( A u. { X } ) ) )
88 15 87 rexlimddv 
 |-  ( ( W e. LVec /\ ( A C_ V /\ Y e. V /\ X e. ( ( N ` ( A u. { Y } ) ) \ ( N ` A ) ) ) ) -> Y e. ( N ` ( A u. { X } ) ) )