Metamath Proof Explorer

Theorem islbs2

Description: An equivalent formulation of the basis predicate in a vector space: a subset is a basis iff no element is in the span of the rest of the set. (Contributed by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs2.v 
|- V = ( Base ` W )
islbs2.j 
|- J = ( LBasis ` W )
islbs2.n 
|- N = ( LSpan ` W )
Assertion islbs2 
|- ( W e. LVec -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs2.v 
 |-  V = ( Base ` W )
2 islbs2.j 
 |-  J = ( LBasis ` W )
3 islbs2.n 
 |-  N = ( LSpan ` W )
4 1 2 lbsss 
 |-  ( B e. J -> B C_ V )
5 4 adantl 
 |-  ( ( W e. LVec /\ B e. J ) -> B C_ V )
6 1 2 3 lbssp 
 |-  ( B e. J -> ( N ` B ) = V )
7 6 adantl 
 |-  ( ( W e. LVec /\ B e. J ) -> ( N ` B ) = V )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
10 9 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
11 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
12 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
13 11 12 drngunz 
 |-  ( ( Scalar ` W ) e. DivRing -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
14 10 13 syl 
 |-  ( W e. LVec -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
15 8 14 jca 
 |-  ( W e. LVec -> ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) )
16 2 3 9 12 11 lbsind2 
 |-  ( ( ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) /\ B e. J /\ x e. B ) -> -. x e. ( N ` ( B \ { x } ) ) )
17 15 16 syl3an1 
 |-  ( ( W e. LVec /\ B e. J /\ x e. B ) -> -. x e. ( N ` ( B \ { x } ) ) )
18 17 3expa 
 |-  ( ( ( W e. LVec /\ B e. J ) /\ x e. B ) -> -. x e. ( N ` ( B \ { x } ) ) )
19 18 ralrimiva 
 |-  ( ( W e. LVec /\ B e. J ) -> A. x e. B -. x e. ( N ` ( B \ { x } ) ) )
20 5 7 19 3jca 
 |-  ( ( W e. LVec /\ B e. J ) -> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) )
21 simpr1 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> B C_ V )
22 simpr2 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> ( N ` B ) = V )
23 id 
 |-  ( x = y -> x = y )
24 sneq 
 |-  ( x = y -> { x } = { y } )
25 24 difeq2d 
 |-  ( x = y -> ( B \ { x } ) = ( B \ { y } ) )
26 25 fveq2d 
 |-  ( x = y -> ( N ` ( B \ { x } ) ) = ( N ` ( B \ { y } ) ) )
27 23 26 eleq12d 
 |-  ( x = y -> ( x e. ( N ` ( B \ { x } ) ) <-> y e. ( N ` ( B \ { y } ) ) ) )
28 27 notbid 
 |-  ( x = y -> ( -. x e. ( N ` ( B \ { x } ) ) <-> -. y e. ( N ` ( B \ { y } ) ) ) )
29 simplr3 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> A. x e. B -. x e. ( N ` ( B \ { x } ) ) )
30 simprl 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> y e. B )
31 28 29 30 rspcdva 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. y e. ( N ` ( B \ { y } ) ) )
32 simpll 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> W e. LVec )
33 simprr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) )
34 eldifsn 
 |-  ( z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) <-> ( z e. ( Base ` ( Scalar ` W ) ) /\ z =/= ( 0g ` ( Scalar ` W ) ) ) )
35 33 34 sylib 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( z e. ( Base ` ( Scalar ` W ) ) /\ z =/= ( 0g ` ( Scalar ` W ) ) ) )
36 21 adantr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> B C_ V )
37 36 30 sseldd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> y e. V )
38 eqid 
 |-  ( .s ` W ) = ( .s ` W )
39 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
40 1 9 38 39 11 3 lspsnvs 
 |-  ( ( W e. LVec /\ ( z e. ( Base ` ( Scalar ` W ) ) /\ z =/= ( 0g ` ( Scalar ` W ) ) ) /\ y e. V ) -> ( N ` { ( z ( .s ` W ) y ) } ) = ( N ` { y } ) )
41 32 35 37 40 syl3anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( N ` { ( z ( .s ` W ) y ) } ) = ( N ` { y } ) )
42 41 sseq1d 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( N ` { ( z ( .s ` W ) y ) } ) C_ ( N ` ( B \ { y } ) ) <-> ( N ` { y } ) C_ ( N ` ( B \ { y } ) ) ) )
43 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
44 8 adantr 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> W e. LMod )
45 44 adantr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> W e. LMod )
46 36 ssdifssd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( B \ { y } ) C_ V )
47 1 43 3 lspcl 
 |-  ( ( W e. LMod /\ ( B \ { y } ) C_ V ) -> ( N ` ( B \ { y } ) ) e. ( LSubSp ` W ) )
48 45 46 47 syl2anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( N ` ( B \ { y } ) ) e. ( LSubSp ` W ) )
49 35 simpld 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> z e. ( Base ` ( Scalar ` W ) ) )
50 1 9 38 39 lmodvscl 
 |-  ( ( W e. LMod /\ z e. ( Base ` ( Scalar ` W ) ) /\ y e. V ) -> ( z ( .s ` W ) y ) e. V )
51 45 49 37 50 syl3anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( z ( .s ` W ) y ) e. V )
52 1 43 3 45 48 51 ellspsn5b 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) <-> ( N ` { ( z ( .s ` W ) y ) } ) C_ ( N ` ( B \ { y } ) ) ) )
53 1 43 3 45 48 37 ellspsn5b 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( y e. ( N ` ( B \ { y } ) ) <-> ( N ` { y } ) C_ ( N ` ( B \ { y } ) ) ) )
54 42 52 53 3bitr4d 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> ( ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) <-> y e. ( N ` ( B \ { y } ) ) ) )
55 31 54 mtbird 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) /\ ( y e. B /\ z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) ) ) -> -. ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) )
56 55 ralrimivva 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> A. y e. B A. z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) )
57 1 9 38 39 2 3 11 islbs 
 |-  ( W e. LVec -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. y e. B A. z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) ) ) )
58 57 adantr 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. y e. B A. z e. ( ( Base ` ( Scalar ` W ) ) \ { ( 0g ` ( Scalar ` W ) ) } ) -. ( z ( .s ` W ) y ) e. ( N ` ( B \ { y } ) ) ) ) )
59 21 22 56 58 mpbir3and 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) -> B e. J )
60 20 59 impbida 
 |-  ( W e. LVec -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) )