Metamath Proof Explorer

Theorem islbs3

Description: An equivalent formulation of the basis predicate: a subset is a basis iff it is a minimal spanning set. (Contributed by Mario Carneiro, 25-Jun-2014)

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

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 8 3ad2ant1 
 |-  ( ( W e. LVec /\ B e. J /\ s C. B ) -> W e. LMod )
10 pssss 
 |-  ( s C. B -> s C_ B )
11 10 4 sylan9ssr 
 |-  ( ( B e. J /\ s C. B ) -> s C_ V )
12 11 3adant1 
 |-  ( ( W e. LVec /\ B e. J /\ s C. B ) -> s C_ V )
13 1 3 lspssv 
 |-  ( ( W e. LMod /\ s C_ V ) -> ( N ` s ) C_ V )
14 9 12 13 syl2anc 
 |-  ( ( W e. LVec /\ B e. J /\ s C. B ) -> ( N ` s ) C_ V )
15 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
16 15 lvecdrng 
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
17 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
18 eqid 
 |-  ( 1r ` ( Scalar ` W ) ) = ( 1r ` ( Scalar ` W ) )
19 17 18 drngunz 
 |-  ( ( Scalar ` W ) e. DivRing -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
20 16 19 syl 
 |-  ( W e. LVec -> ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) )
21 8 20 jca 
 |-  ( W e. LVec -> ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) )
22 2 3 15 18 17 1 lbspss 
 |-  ( ( ( W e. LMod /\ ( 1r ` ( Scalar ` W ) ) =/= ( 0g ` ( Scalar ` W ) ) ) /\ B e. J /\ s C. B ) -> ( N ` s ) =/= V )
23 21 22 syl3an1 
 |-  ( ( W e. LVec /\ B e. J /\ s C. B ) -> ( N ` s ) =/= V )
24 df-pss 
 |-  ( ( N ` s ) C. V <-> ( ( N ` s ) C_ V /\ ( N ` s ) =/= V ) )
25 14 23 24 sylanbrc 
 |-  ( ( W e. LVec /\ B e. J /\ s C. B ) -> ( N ` s ) C. V )
26 25 3expia 
 |-  ( ( W e. LVec /\ B e. J ) -> ( s C. B -> ( N ` s ) C. V ) )
27 26 alrimiv 
 |-  ( ( W e. LVec /\ B e. J ) -> A. s ( s C. B -> ( N ` s ) C. V ) )
28 5 7 27 3jca 
 |-  ( ( W e. LVec /\ B e. J ) -> ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) )
29 simpr1 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) -> B C_ V )
30 simpr2 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) -> ( N ` B ) = V )
31 simplr1 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> B C_ V )
32 31 ssdifssd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( B \ { x } ) C_ V )
33 1 fvexi 
 |-  V e. _V
34 ssexg 
 |-  ( ( ( B \ { x } ) C_ V /\ V e. _V ) -> ( B \ { x } ) e. _V )
35 32 33 34 sylancl 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( B \ { x } ) e. _V )
36 simplr3 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> A. s ( s C. B -> ( N ` s ) C. V ) )
37 difssd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( B \ { x } ) C_ B )
38 simpr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> x e. B )
39 neldifsn 
 |-  -. x e. ( B \ { x } )
40 nelne1 
 |-  ( ( x e. B /\ -. x e. ( B \ { x } ) ) -> B =/= ( B \ { x } ) )
41 38 39 40 sylancl 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> B =/= ( B \ { x } ) )
42 41 necomd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( B \ { x } ) =/= B )
43 df-pss 
 |-  ( ( B \ { x } ) C. B <-> ( ( B \ { x } ) C_ B /\ ( B \ { x } ) =/= B ) )
44 37 42 43 sylanbrc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( B \ { x } ) C. B )
45 psseq1 
 |-  ( s = ( B \ { x } ) -> ( s C. B <-> ( B \ { x } ) C. B ) )
46 fveq2 
 |-  ( s = ( B \ { x } ) -> ( N ` s ) = ( N ` ( B \ { x } ) ) )
47 46 psseq1d 
 |-  ( s = ( B \ { x } ) -> ( ( N ` s ) C. V <-> ( N ` ( B \ { x } ) ) C. V ) )
48 45 47 imbi12d 
 |-  ( s = ( B \ { x } ) -> ( ( s C. B -> ( N ` s ) C. V ) <-> ( ( B \ { x } ) C. B -> ( N ` ( B \ { x } ) ) C. V ) ) )
49 48 spcgv 
 |-  ( ( B \ { x } ) e. _V -> ( A. s ( s C. B -> ( N ` s ) C. V ) -> ( ( B \ { x } ) C. B -> ( N ` ( B \ { x } ) ) C. V ) ) )
50 35 36 44 49 syl3c 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( N ` ( B \ { x } ) ) C. V )
51 dfpss3 
 |-  ( ( N ` ( B \ { x } ) ) C. V <-> ( ( N ` ( B \ { x } ) ) C_ V /\ -. V C_ ( N ` ( B \ { x } ) ) ) )
52 51 simprbi 
 |-  ( ( N ` ( B \ { x } ) ) C. V -> -. V C_ ( N ` ( B \ { x } ) ) )
53 50 52 syl 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> -. V C_ ( N ` ( B \ { x } ) ) )
54 simplr2 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( N ` B ) = V )
55 8 ad2antrr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> W e. LMod )
56 32 adantrr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( B \ { x } ) C_ V )
57 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
58 1 57 3 lspcl 
 |-  ( ( W e. LMod /\ ( B \ { x } ) C_ V ) -> ( N ` ( B \ { x } ) ) e. ( LSubSp ` W ) )
59 55 56 58 syl2anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( N ` ( B \ { x } ) ) e. ( LSubSp ` W ) )
60 ssun1 
 |-  B C_ ( B u. { x } )
61 undif1 
 |-  ( ( B \ { x } ) u. { x } ) = ( B u. { x } )
62 60 61 sseqtrri 
 |-  B C_ ( ( B \ { x } ) u. { x } )
63 1 3 lspssid 
 |-  ( ( W e. LMod /\ ( B \ { x } ) C_ V ) -> ( B \ { x } ) C_ ( N ` ( B \ { x } ) ) )
64 55 56 63 syl2anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( B \ { x } ) C_ ( N ` ( B \ { x } ) ) )
65 simprr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> x e. ( N ` ( B \ { x } ) ) )
66 65 snssd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> { x } C_ ( N ` ( B \ { x } ) ) )
67 64 66 unssd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( ( B \ { x } ) u. { x } ) C_ ( N ` ( B \ { x } ) ) )
68 62 67 sstrid 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> B C_ ( N ` ( B \ { x } ) ) )
69 57 3 lspssp 
 |-  ( ( W e. LMod /\ ( N ` ( B \ { x } ) ) e. ( LSubSp ` W ) /\ B C_ ( N ` ( B \ { x } ) ) ) -> ( N ` B ) C_ ( N ` ( B \ { x } ) ) )
70 55 59 68 69 syl3anc 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> ( N ` B ) C_ ( N ` ( B \ { x } ) ) )
71 54 70 eqsstrrd 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ ( x e. B /\ x e. ( N ` ( B \ { x } ) ) ) ) -> V C_ ( N ` ( B \ { x } ) ) )
72 71 expr 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> ( x e. ( N ` ( B \ { x } ) ) -> V C_ ( N ` ( B \ { x } ) ) ) )
73 53 72 mtod 
 |-  ( ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) /\ x e. B ) -> -. x e. ( N ` ( B \ { x } ) ) )
74 73 ralrimiva 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) -> A. x e. B -. x e. ( N ` ( B \ { x } ) ) )
75 1 2 3 islbs2 
 |-  ( W e. LVec -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) )
76 75 adantr 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. x e. B -. x e. ( N ` ( B \ { x } ) ) ) ) )
77 29 30 74 76 mpbir3and 
 |-  ( ( W e. LVec /\ ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) -> B e. J )
78 28 77 impbida 
 |-  ( W e. LVec -> ( B e. J <-> ( B C_ V /\ ( N ` B ) = V /\ A. s ( s C. B -> ( N ` s ) C. V ) ) ) )