Metamath Proof Explorer

Theorem lbsacsbs

Description: Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses lbsacsbs.1 
|- A = ( LSubSp ` W )
lbsacsbs.2 
|- N = ( mrCls ` A )
lbsacsbs.3 
|- X = ( Base ` W )
lbsacsbs.4 
|- I = ( mrInd ` A )
lbsacsbs.5 
|- J = ( LBasis ` W )
Assertion lbsacsbs 
|- ( W e. LVec -> ( S e. J <-> ( S e. I /\ ( N ` S ) = X ) ) )

Proof

Step Hyp Ref Expression
1 lbsacsbs.1 
 |-  A = ( LSubSp ` W )
2 lbsacsbs.2 
 |-  N = ( mrCls ` A )
3 lbsacsbs.3 
 |-  X = ( Base ` W )
4 lbsacsbs.4 
 |-  I = ( mrInd ` A )
5 lbsacsbs.5 
 |-  J = ( LBasis ` W )
6 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
7 3 5 6 islbs2 
 |-  ( W e. LVec -> ( S e. J <-> ( S C_ X /\ ( ( LSpan ` W ) ` S ) = X /\ A. x e. S -. x e. ( ( LSpan ` W ) ` ( S \ { x } ) ) ) ) )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 1 6 2 mrclsp 
 |-  ( W e. LMod -> ( LSpan ` W ) = N )
10 8 9 syl 
 |-  ( W e. LVec -> ( LSpan ` W ) = N )
11 10 fveq1d 
 |-  ( W e. LVec -> ( ( LSpan ` W ) ` S ) = ( N ` S ) )
12 11 eqeq1d 
 |-  ( W e. LVec -> ( ( ( LSpan ` W ) ` S ) = X <-> ( N ` S ) = X ) )
13 10 fveq1d 
 |-  ( W e. LVec -> ( ( LSpan ` W ) ` ( S \ { x } ) ) = ( N ` ( S \ { x } ) ) )
14 13 eleq2d 
 |-  ( W e. LVec -> ( x e. ( ( LSpan ` W ) ` ( S \ { x } ) ) <-> x e. ( N ` ( S \ { x } ) ) ) )
15 14 notbid 
 |-  ( W e. LVec -> ( -. x e. ( ( LSpan ` W ) ` ( S \ { x } ) ) <-> -. x e. ( N ` ( S \ { x } ) ) ) )
16 15 ralbidv 
 |-  ( W e. LVec -> ( A. x e. S -. x e. ( ( LSpan ` W ) ` ( S \ { x } ) ) <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
17 12 16 3anbi23d 
 |-  ( W e. LVec -> ( ( S C_ X /\ ( ( LSpan ` W ) ` S ) = X /\ A. x e. S -. x e. ( ( LSpan ` W ) ` ( S \ { x } ) ) ) <-> ( S C_ X /\ ( N ` S ) = X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) )
18 3anan32 
 |-  ( ( S C_ X /\ ( N ` S ) = X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) <-> ( ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) /\ ( N ` S ) = X ) )
19 3 1 lssmre 
 |-  ( W e. LMod -> A e. ( Moore ` X ) )
20 2 4 ismri 
 |-  ( A e. ( Moore ` X ) -> ( S e. I <-> ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) )
21 8 19 20 3syl 
 |-  ( W e. LVec -> ( S e. I <-> ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) ) )
22 21 anbi1d 
 |-  ( W e. LVec -> ( ( S e. I /\ ( N ` S ) = X ) <-> ( ( S C_ X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) /\ ( N ` S ) = X ) ) )
23 18 22 bitr4id 
 |-  ( W e. LVec -> ( ( S C_ X /\ ( N ` S ) = X /\ A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) <-> ( S e. I /\ ( N ` S ) = X ) ) )
24 7 17 23 3bitrd 
 |-  ( W e. LVec -> ( S e. J <-> ( S e. I /\ ( N ` S ) = X ) ) )