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 → ( 𝑆 ∈ 𝐽 ↔ ( 𝑆 ∈ 𝐼 ∧ ( 𝑁 ‘ 𝑆 ) = 𝑋 ) ) )