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 ∈ LVec → S ∈ J ↔ S ∈ 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 ∈ LVec → S ∈ J ↔ S ⊆ X ∧ LSpan ⁡ W ⁡ S = X ∧ ∀ x ∈ S ¬ x ∈ LSpan ⁡ W ⁡ S ∖ x
8 lveclmod ⊢ W ∈ LVec → W ∈ LMod
9 1 6 2 mrclsp ⊢ W ∈ LMod → LSpan ⁡ W = N
10 8 9 syl ⊢ W ∈ LVec → LSpan ⁡ W = N
11 10 fveq1d ⊢ W ∈ LVec → LSpan ⁡ W ⁡ S = N ⁡ S
12 11 eqeq1d ⊢ W ∈ LVec → LSpan ⁡ W ⁡ S = X ↔ N ⁡ S = X
13 10 fveq1d ⊢ W ∈ LVec → LSpan ⁡ W ⁡ S ∖ x = N ⁡ S ∖ x
14 13 eleq2d ⊢ W ∈ LVec → x ∈ LSpan ⁡ W ⁡ S ∖ x ↔ x ∈ N ⁡ S ∖ x
15 14 notbid ⊢ W ∈ LVec → ¬ x ∈ LSpan ⁡ W ⁡ S ∖ x ↔ ¬ x ∈ N ⁡ S ∖ x
16 15 ralbidv ⊢ W ∈ LVec → ∀ x ∈ S ¬ x ∈ LSpan ⁡ W ⁡ S ∖ x ↔ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
17 12 16 3anbi23d ⊢ W ∈ LVec → S ⊆ X ∧ LSpan ⁡ W ⁡ S = X ∧ ∀ x ∈ S ¬ x ∈ LSpan ⁡ W ⁡ S ∖ x ↔ S ⊆ X ∧ N ⁡ S = X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
18 3anan32 ⊢ S ⊆ X ∧ N ⁡ S = X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x ∧ N ⁡ S = X
19 3 1 lssmre ⊢ W ∈ LMod → A ∈ Moore ⁡ X
20 2 4 ismri ⊢ A ∈ Moore ⁡ X → S ∈ I ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
21 8 19 20 3syl ⊢ W ∈ LVec → S ∈ I ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
22 21 anbi1d ⊢ W ∈ LVec → S ∈ I ∧ N ⁡ S = X ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x ∧ N ⁡ S = X
23 18 22 bitr4id ⊢ W ∈ LVec → S ⊆ X ∧ N ⁡ S = X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x ↔ S ∈ I ∧ N ⁡ S = X
24 7 17 23 3bitrd ⊢ W ∈ LVec → S ∈ J ↔ S ∈ I ∧ N ⁡ S = X