MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lspsolv Structured version   Visualization version   Unicode version

Theorem lspsolv 18414
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.)
Hypotheses
Ref Expression
lspsolv.v  |-  V  =  ( Base `  W
)
lspsolv.s  |-  S  =  ( LSubSp `  W )
lspsolv.n  |-  N  =  ( LSpan `  W )
Assertion
Ref Expression
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 of Theorem lspsolv
Dummy variables  r 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lspsolv.v . . 3  |-  V  =  ( Base `  W
)
2 lspsolv.s . . 3  |-  S  =  ( LSubSp `  W )
3 lspsolv.n . . 3  |-  N  =  ( LSpan `  W )
4 eqid 2461 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2461 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2461 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
7 eqid 2461 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
8 eqid 2461 . . 3  |-  { 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 18377 . . . 4  |-  ( W  e.  LVec  ->  W  e. 
LMod )
109adantr 471 . . 3  |-  ( ( W  e.  LVec  /\  ( A  C_  V  /\  Y  e.  V  /\  X  e.  ( ( N `  ( A  u.  { Y } ) )  \ 
( N `  A
) ) ) )  ->  W  e.  LMod )
11 simpr1 1020 . . 3  |-  ( ( W  e.  LVec  /\  ( A  C_  V  /\  Y  e.  V  /\  X  e.  ( ( N `  ( A  u.  { Y } ) )  \ 
( N `  A
) ) ) )  ->  A  C_  V
)
12 simpr2 1021 . . 3  |-  ( ( W  e.  LVec  /\  ( A  C_  V  /\  Y  e.  V  /\  X  e.  ( ( N `  ( A  u.  { Y } ) )  \ 
( N `  A
) ) ) )  ->  Y  e.  V
)
13 simpr3 1022 . . . 4  |-  ( ( 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
) ) )
1413eldifad 3427 . . 3  |-  ( ( W  e.  LVec  /\  ( A  C_  V  /\  Y  e.  V  /\  X  e.  ( ( N `  ( A  u.  { Y } ) )  \ 
( N `  A
) ) ) )  ->  X  e.  ( N `  ( A  u.  { Y }
) ) )
151, 2, 3, 4, 5, 6, 7, 8, 10, 11, 12, 14lspsolvlem 18413 . 2  |-  ( ( 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
) )
164lvecdrng 18376 . . . . . . 7  |-  ( W  e.  LVec  ->  (Scalar `  W )  e.  DivRing )
1716ad2antrr 737 . . . . . 6  |-  ( ( ( 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 769 . . . . . 6  |-  ( ( ( 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 )
) )
1910adantr 471 . . . . . . . . . . . 12  |-  ( ( ( 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 )
2012adantr 471 . . . . . . . . . . . 12  |-  ( ( ( 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 2461 . . . . . . . . . . . . 13  |-  ( 0g
`  (Scalar `  W )
)  =  ( 0g
`  (Scalar `  W )
)
22 eqid 2461 . . . . . . . . . . . . 13  |-  ( 0g
`  W )  =  ( 0g `  W
)
231, 4, 7, 21, 22lmod0vs 18172 . . . . . . . . . . . 12  |-  ( ( W  e.  LMod  /\  Y  e.  V )  ->  (
( 0g `  (Scalar `  W ) ) ( .s `  W ) Y )  =  ( 0g `  W ) )
2419, 20, 23syl2anc 671 . . . . . . . . . . 11  |-  ( ( ( 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
) )
2524oveq2d 6330 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
2611adantr 471 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
2720snssd 4129 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
)
2826, 27unssd 3621 . . . . . . . . . . . . . 14  |-  ( ( ( 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
)
291, 3lspssv 18254 . . . . . . . . . . . . . 14  |-  ( ( W  e.  LMod  /\  ( A  u.  { Y } )  C_  V
)  ->  ( N `  ( A  u.  { Y } ) )  C_  V )
3019, 28, 29syl2anc 671 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
3130ssdifssd 3582 . . . . . . . . . . . 12  |-  ( ( ( 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
)
3213adantr 471 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
3331, 32sseldd 3444 . . . . . . . . . . 11  |-  ( ( ( 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 )
341, 6, 22lmod0vrid 18170 . . . . . . . . . . 11  |-  ( ( W  e.  LMod  /\  X  e.  V )  ->  ( X ( +g  `  W
) ( 0g `  W ) )  =  X )
3519, 33, 34syl2anc 671 . . . . . . . . . 10  |-  ( ( ( 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 )
3625, 35eqtrd 2495 . . . . . . . . 9  |-  ( ( ( 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 )
3736, 32eqeltrd 2539 . . . . . . . 8  |-  ( ( ( 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
) ) )
3837eldifbd 3428 . . . . . . 7  |-  ( ( ( 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 771 . . . . . . . . 9  |-  ( ( ( 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 6321 . . . . . . . . . . 11  |-  ( r  =  ( 0g `  (Scalar `  W ) )  ->  ( r ( .s `  W ) Y )  =  ( ( 0g `  (Scalar `  W ) ) ( .s `  W ) Y ) )
4140oveq2d 6330 . . . . . . . . . 10  |-  ( r  =  ( 0g `  (Scalar `  W ) )  ->  ( X ( +g  `  W ) ( r ( .s
`  W ) Y ) )  =  ( X ( +g  `  W
) ( ( 0g
`  (Scalar `  W )
) ( .s `  W ) Y ) ) )
4241eleq1d 2523 . . . . . . . . 9  |-  ( 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 ) ) )
4339, 42syl5ibcom 228 . . . . . . . 8  |-  ( ( ( 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
) ) )
4443necon3bd 2649 . . . . . . 7  |-  ( ( ( 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 )
) ) )
4538, 44mpd 15 . . . . . 6  |-  ( ( ( 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 2461 . . . . . . 7  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
47 eqid 2461 . . . . . . 7  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
48 eqid 2461 . . . . . . 7  |-  ( invr `  (Scalar `  W )
)  =  ( invr `  (Scalar `  W )
)
495, 21, 46, 47, 48drnginvrl 18042 . . . . . 6  |-  ( ( (Scalar `  W )  e.  DivRing  /\  r  e.  ( Base `  (Scalar `  W
) )  /\  r  =/=  ( 0g `  (Scalar `  W ) ) )  ->  ( ( (
invr `  (Scalar `  W
) ) `  r
) ( .r `  (Scalar `  W ) ) r )  =  ( 1r `  (Scalar `  W ) ) )
5017, 18, 45, 49syl3anc 1276 . . . . 5  |-  ( ( ( 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 )
) )
5150oveq1d 6329 . . . 4  |-  ( ( ( 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 ) )
525, 21, 48drnginvrcl 18040 . . . . . 6  |-  ( ( (Scalar `  W )  e.  DivRing  /\  r  e.  ( Base `  (Scalar `  W
) )  /\  r  =/=  ( 0g `  (Scalar `  W ) ) )  ->  ( ( invr `  (Scalar `  W )
) `  r )  e.  ( Base `  (Scalar `  W ) ) )
5317, 18, 45, 52syl3anc 1276 . . . . 5  |-  ( ( ( 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
) ) )
541, 4, 7, 5, 46lmodvsass 18164 . . . . 5  |-  ( ( 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 ) ) )
5519, 53, 18, 20, 54syl13anc 1278 . . . 4  |-  ( ( ( 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 ) ) )
561, 4, 7, 47lmodvs1 18167 . . . . 5  |-  ( ( W  e.  LMod  /\  Y  e.  V )  ->  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) Y )  =  Y )
5719, 20, 56syl2anc 671 . . . 4  |-  ( ( ( 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 )
5851, 55, 573eqtr3d 2503 . . 3  |-  ( ( ( 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 )
5933snssd 4129 . . . . . 6  |-  ( ( ( 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
)
6026, 59unssd 3621 . . . . 5  |-  ( ( ( 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
)
611, 2, 3lspcl 18247 . . . . 5  |-  ( ( W  e.  LMod  /\  ( A  u.  { X } )  C_  V
)  ->  ( N `  ( A  u.  { X } ) )  e.  S )
6219, 60, 61syl2anc 671 . . . 4  |-  ( ( ( 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 )
631, 4, 7, 5lmodvscl 18156 . . . . . . 7  |-  ( ( W  e.  LMod  /\  r  e.  ( Base `  (Scalar `  W ) )  /\  Y  e.  V )  ->  ( r ( .s
`  W ) Y )  e.  V )
6419, 18, 20, 63syl3anc 1276 . . . . . 6  |-  ( ( ( 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 2461 . . . . . . 7  |-  ( -g `  W )  =  (
-g `  W )
661, 6, 65lmodvpncan 18189 . . . . . 6  |-  ( ( 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 ) )
6719, 64, 33, 66syl3anc 1276 . . . . 5  |-  ( ( ( 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 ) )
681, 6lmodcom 18182 . . . . . . . 8  |-  ( ( 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 ) ) )
6919, 64, 33, 68syl3anc 1276 . . . . . . 7  |-  ( ( ( 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 3608 . . . . . . . . . 10  |-  A  C_  ( A  u.  { X } )
7170a1i 11 . . . . . . . . 9  |-  ( ( ( 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 } ) )
721, 3lspss 18255 . . . . . . . . 9  |-  ( ( W  e.  LMod  /\  ( A  u.  { X } )  C_  V  /\  A  C_  ( A  u.  { X }
) )  ->  ( N `  A )  C_  ( N `  ( A  u.  { X } ) ) )
7319, 60, 71, 72syl3anc 1276 . . . . . . . 8  |-  ( ( ( 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 } ) ) )
7473, 39sseldd 3444 . . . . . . 7  |-  ( ( ( 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 } ) ) )
7569, 74eqeltrd 2539 . . . . . 6  |-  ( ( ( 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 } ) ) )
761, 3lspssid 18256 . . . . . . . 8  |-  ( ( W  e.  LMod  /\  ( A  u.  { X } )  C_  V
)  ->  ( A  u.  { X } ) 
C_  ( N `  ( A  u.  { X } ) ) )
7719, 60, 76syl2anc 671 . . . . . . 7  |-  ( ( ( 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 4005 . . . . . . . 8  |-  ( X  e.  V  ->  X  e.  { X } )
79 elun2 3613 . . . . . . . 8  |-  ( X  e.  { X }  ->  X  e.  ( A  u.  { X }
) )
8033, 78, 793syl 18 . . . . . . 7  |-  ( ( ( 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 } ) )
8177, 80sseldd 3444 . . . . . 6  |-  ( ( ( 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 } ) ) )
8265, 2lssvsubcl 18215 . . . . . 6  |-  ( ( ( 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 }
) ) )
8319, 62, 75, 81, 82syl22anc 1277 . . . . 5  |-  ( ( ( 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 } ) ) )
8467, 83eqeltrrd 2540 . . . 4  |-  ( ( ( 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 } ) ) )
854, 7, 5, 2lssvscl 18226 . . . 4  |-  ( ( ( 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 } ) ) )
8619, 62, 53, 84, 85syl22anc 1277 . . 3  |-  ( ( ( 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 } ) ) )
8758, 86eqeltrrd 2540 . 2  |-  ( ( ( 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 } ) ) )
8815, 87rexlimddv 2894 1  |-  ( ( W  e.  LVec  /\  ( A  C_  V  /\  Y  e.  V  /\  X  e.  ( ( N `  ( A  u.  { Y } ) )  \ 
( N `  A
) ) ) )  ->  Y  e.  ( N `  ( A  u.  { X }
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375    /\ w3a 991    = wceq 1454    e. wcel 1897    =/= wne 2632   E.wrex 2749   {crab 2752    \ cdif 3412    u. cun 3413    C_ wss 3415   {csn 3979   ` cfv 5600  (class class class)co 6314   Basecbs 15169   +g cplusg 15238   .rcmulr 15239  Scalarcsca 15241   .scvsca 15242   0gc0g 15386   -gcsg 16719   1rcur 17783   invrcinvr 17947   DivRingcdr 18023   LModclmod 18139   LSubSpclss 18203   LSpanclspn 18242   LVecclvec 18373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-tpos 6998  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-er 7388  df-en 7595  df-dom 7596  df-sdom 7597  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-nn 10637  df-2 10695  df-3 10696  df-ndx 15172  df-slot 15173  df-base 15174  df-sets 15175  df-ress 15176  df-plusg 15251  df-mulr 15252  df-0g 15388  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-grp 16721  df-minusg 16722  df-sbg 16723  df-cmn 17480  df-abl 17481  df-mgp 17772  df-ur 17784  df-ring 17830  df-oppr 17899  df-dvdsr 17917  df-unit 17918  df-invr 17948  df-drng 18025  df-lmod 18141  df-lss 18204  df-lsp 18243  df-lvec 18374
This theorem is referenced by:  lssacsex  18415  lspsnat  18416  lsppratlem1  18418  lsppratlem3  18420  lsppratlem4  18421  lbsextlem4  18432
  Copyright terms: Public domain W3C validator