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 𝐴 = ( LSubSp ‘ 𝑊 )
lbsacsbs.2 𝑁 = ( mrCls ‘ 𝐴 )
lbsacsbs.3 𝑋 = ( Base ‘ 𝑊 )
lbsacsbs.4 𝐼 = ( mrInd ‘ 𝐴 )
lbsacsbs.5 𝐽 = ( LBasis ‘ 𝑊 )
Assertion lbsacsbs ( 𝑊 ∈ LVec → ( 𝑆𝐽 ↔ ( 𝑆𝐼 ∧ ( 𝑁𝑆 ) = 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lbsacsbs.1 𝐴 = ( LSubSp ‘ 𝑊 )
2 lbsacsbs.2 𝑁 = ( mrCls ‘ 𝐴 )
3 lbsacsbs.3 𝑋 = ( Base ‘ 𝑊 )
4 lbsacsbs.4 𝐼 = ( mrInd ‘ 𝐴 )
5 lbsacsbs.5 𝐽 = ( LBasis ‘ 𝑊 )
6 eqid ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
7 3 5 6 islbs2 ( 𝑊 ∈ LVec → ( 𝑆𝐽 ↔ ( 𝑆𝑋 ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝑆 ) = 𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
8 lveclmod ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 1 6 2 mrclsp ( 𝑊 ∈ LMod → ( LSpan ‘ 𝑊 ) = 𝑁 )
10 8 9 syl ( 𝑊 ∈ LVec → ( LSpan ‘ 𝑊 ) = 𝑁 )
11 10 fveq1d ( 𝑊 ∈ LVec → ( ( LSpan ‘ 𝑊 ) ‘ 𝑆 ) = ( 𝑁𝑆 ) )
12 11 eqeq1d ( 𝑊 ∈ LVec → ( ( ( LSpan ‘ 𝑊 ) ‘ 𝑆 ) = 𝑋 ↔ ( 𝑁𝑆 ) = 𝑋 ) )
13 10 fveq1d ( 𝑊 ∈ LVec → ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
14 13 eleq2d ( 𝑊 ∈ LVec → ( 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
15 14 notbid ( 𝑊 ∈ LVec → ( ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
16 15 ralbidv ( 𝑊 ∈ LVec → ( ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
17 12 16 3anbi23d ( 𝑊 ∈ LVec → ( ( 𝑆𝑋 ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝑆 ) = 𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( 𝑆𝑋 ∧ ( 𝑁𝑆 ) = 𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
18 3anan32 ( ( 𝑆𝑋 ∧ ( 𝑁𝑆 ) = 𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑆𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ∧ ( 𝑁𝑆 ) = 𝑋 ) )
19 3 1 lssmre ( 𝑊 ∈ LMod → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
20 2 4 ismri ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆𝐼 ↔ ( 𝑆𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
21 8 19 20 3syl ( 𝑊 ∈ LVec → ( 𝑆𝐼 ↔ ( 𝑆𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
22 21 anbi1d ( 𝑊 ∈ LVec → ( ( 𝑆𝐼 ∧ ( 𝑁𝑆 ) = 𝑋 ) ↔ ( ( 𝑆𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ∧ ( 𝑁𝑆 ) = 𝑋 ) ) )
23 18 22 bitr4id ( 𝑊 ∈ LVec → ( ( 𝑆𝑋 ∧ ( 𝑁𝑆 ) = 𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( 𝑆𝐼 ∧ ( 𝑁𝑆 ) = 𝑋 ) ) )
24 7 17 23 3bitrd ( 𝑊 ∈ LVec → ( 𝑆𝐽 ↔ ( 𝑆𝐼 ∧ ( 𝑁𝑆 ) = 𝑋 ) ) )