Metamath Proof Explorer

Theorem islinds4

Description: A set is independent in a vector space iff it is a subset of some basis. This is an axiom of choice equivalent. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis islinds4.j ⊢ J = LBasis ⁡ W
Assertion islinds4 ⊢ W ∈ LVec → Y ∈ LIndS ⁡ W ↔ ∃ b ∈ J Y ⊆ b

Proof

Step Hyp Ref Expression
1 islinds4.j ⊢ J = LBasis ⁡ W
2 simpl ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W → W ∈ LVec
3 eqid ⊢ Base W = Base W
4 3 linds1 ⊢ Y ∈ LIndS ⁡ W → Y ⊆ Base W
5 4 adantl ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W → Y ⊆ Base W
6 lveclmod ⊢ W ∈ LVec → W ∈ LMod
7 6 ad2antrr ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → W ∈ LMod
8 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
9 8 lvecdrng ⊢ W ∈ LVec → Scalar ⁡ W ∈ DivRing
10 drngnzr ⊢ Scalar ⁡ W ∈ DivRing → Scalar ⁡ W ∈ NzRing
11 9 10 syl ⊢ W ∈ LVec → Scalar ⁡ W ∈ NzRing
12 11 ad2antrr ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → Scalar ⁡ W ∈ NzRing
13 simplr ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → Y ∈ LIndS ⁡ W
14 simpr ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → x ∈ Y
15 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
16 15 8 lindsind2 ⊢ W ∈ LMod ∧ Scalar ⁡ W ∈ NzRing ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → ¬ x ∈ LSpan ⁡ W ⁡ Y ∖ x
17 7 12 13 14 16 syl211anc ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W ∧ x ∈ Y → ¬ x ∈ LSpan ⁡ W ⁡ Y ∖ x
18 17 ralrimiva ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W → ∀ x ∈ Y ¬ x ∈ LSpan ⁡ W ⁡ Y ∖ x
19 1 3 15 lbsext ⊢ W ∈ LVec ∧ Y ⊆ Base W ∧ ∀ x ∈ Y ¬ x ∈ LSpan ⁡ W ⁡ Y ∖ x → ∃ b ∈ J Y ⊆ b
20 2 5 18 19 syl3anc ⊢ W ∈ LVec ∧ Y ∈ LIndS ⁡ W → ∃ b ∈ J Y ⊆ b
21 20 ex ⊢ W ∈ LVec → Y ∈ LIndS ⁡ W → ∃ b ∈ J Y ⊆ b
22 6 ad2antrr ⊢ W ∈ LVec ∧ b ∈ J ∧ Y ⊆ b → W ∈ LMod
23 1 lbslinds ⊢ J ⊆ LIndS ⁡ W
24 23 sseli ⊢ b ∈ J → b ∈ LIndS ⁡ W
25 24 ad2antlr ⊢ W ∈ LVec ∧ b ∈ J ∧ Y ⊆ b → b ∈ LIndS ⁡ W
26 simpr ⊢ W ∈ LVec ∧ b ∈ J ∧ Y ⊆ b → Y ⊆ b
27 lindsss ⊢ W ∈ LMod ∧ b ∈ LIndS ⁡ W ∧ Y ⊆ b → Y ∈ LIndS ⁡ W
28 22 25 26 27 syl3anc ⊢ W ∈ LVec ∧ b ∈ J ∧ Y ⊆ b → Y ∈ LIndS ⁡ W
29 28 rexlimdva2 ⊢ W ∈ LVec → ∃ b ∈ J Y ⊆ b → Y ∈ LIndS ⁡ W
30 21 29 impbid ⊢ W ∈ LVec → Y ∈ LIndS ⁡ W ↔ ∃ b ∈ J Y ⊆ b