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=BaseW
islbs2.j J=LBasisW
islbs2.n N=LSpanW
Assertion islbs3 WLVecBJBVNB=VssBNsV

Proof

Step Hyp Ref Expression
1 islbs2.v V=BaseW
2 islbs2.j J=LBasisW
3 islbs2.n N=LSpanW
4 1 2 lbsss BJBV
5 4 adantl WLVecBJBV
6 1 2 3 lbssp BJNB=V
7 6 adantl WLVecBJNB=V
8 lveclmod WLVecWLMod
9 8 3ad2ant1 WLVecBJsBWLMod
10 pssss sBsB
11 10 4 sylan9ssr BJsBsV
12 11 3adant1 WLVecBJsBsV
13 1 3 lspssv WLModsVNsV
14 9 12 13 syl2anc WLVecBJsBNsV
15 eqid ScalarW=ScalarW
16 15 lvecdrng WLVecScalarWDivRing
17 eqid 0ScalarW=0ScalarW
18 eqid 1ScalarW=1ScalarW
19 17 18 drngunz ScalarWDivRing1ScalarW0ScalarW
20 16 19 syl WLVec1ScalarW0ScalarW
21 8 20 jca WLVecWLMod1ScalarW0ScalarW
22 2 3 15 18 17 1 lbspss WLMod1ScalarW0ScalarWBJsBNsV
23 21 22 syl3an1 WLVecBJsBNsV
24 df-pss NsVNsVNsV
25 14 23 24 sylanbrc WLVecBJsBNsV
26 25 3expia WLVecBJsBNsV
27 26 alrimiv WLVecBJssBNsV
28 5 7 27 3jca WLVecBJBVNB=VssBNsV
29 simpr1 WLVecBVNB=VssBNsVBV
30 simpr2 WLVecBVNB=VssBNsVNB=V
31 simplr1 WLVecBVNB=VssBNsVxBBV
32 31 ssdifssd WLVecBVNB=VssBNsVxBBxV
33 1 fvexi VV
34 ssexg BxVVVBxV
35 32 33 34 sylancl WLVecBVNB=VssBNsVxBBxV
36 simplr3 WLVecBVNB=VssBNsVxBssBNsV
37 difssd WLVecBVNB=VssBNsVxBBxB
38 simpr WLVecBVNB=VssBNsVxBxB
39 neldifsn ¬xBx
40 nelne1 xB¬xBxBBx
41 38 39 40 sylancl WLVecBVNB=VssBNsVxBBBx
42 41 necomd WLVecBVNB=VssBNsVxBBxB
43 df-pss BxBBxBBxB
44 37 42 43 sylanbrc WLVecBVNB=VssBNsVxBBxB
45 psseq1 s=BxsBBxB
46 fveq2 s=BxNs=NBx
47 46 psseq1d s=BxNsVNBxV
48 45 47 imbi12d s=BxsBNsVBxBNBxV
49 48 spcgv BxVssBNsVBxBNBxV
50 35 36 44 49 syl3c WLVecBVNB=VssBNsVxBNBxV
51 dfpss3 NBxVNBxV¬VNBx
52 51 simprbi NBxV¬VNBx
53 50 52 syl WLVecBVNB=VssBNsVxB¬VNBx
54 simplr2 WLVecBVNB=VssBNsVxBxNBxNB=V
55 8 ad2antrr WLVecBVNB=VssBNsVxBxNBxWLMod
56 32 adantrr WLVecBVNB=VssBNsVxBxNBxBxV
57 eqid LSubSpW=LSubSpW
58 1 57 3 lspcl WLModBxVNBxLSubSpW
59 55 56 58 syl2anc WLVecBVNB=VssBNsVxBxNBxNBxLSubSpW
60 ssun1 BBx
61 undif1 Bxx=Bx
62 60 61 sseqtrri BBxx
63 1 3 lspssid WLModBxVBxNBx
64 55 56 63 syl2anc WLVecBVNB=VssBNsVxBxNBxBxNBx
65 simprr WLVecBVNB=VssBNsVxBxNBxxNBx
66 65 snssd WLVecBVNB=VssBNsVxBxNBxxNBx
67 64 66 unssd WLVecBVNB=VssBNsVxBxNBxBxxNBx
68 62 67 sstrid WLVecBVNB=VssBNsVxBxNBxBNBx
69 57 3 lspssp WLModNBxLSubSpWBNBxNBNBx
70 55 59 68 69 syl3anc WLVecBVNB=VssBNsVxBxNBxNBNBx
71 54 70 eqsstrrd WLVecBVNB=VssBNsVxBxNBxVNBx
72 71 expr WLVecBVNB=VssBNsVxBxNBxVNBx
73 53 72 mtod WLVecBVNB=VssBNsVxB¬xNBx
74 73 ralrimiva WLVecBVNB=VssBNsVxB¬xNBx
75 1 2 3 islbs2 WLVecBJBVNB=VxB¬xNBx
76 75 adantr WLVecBVNB=VssBNsVBJBVNB=VxB¬xNBx
77 29 30 74 76 mpbir3and WLVecBVNB=VssBNsVBJ
78 28 77 impbida WLVecBJBVNB=VssBNsV