This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion islinds4 ( 𝑊 ∈ LVec → ( 𝑌 ∈ ( LIndS ‘ 𝑊 ) ↔ ∃ 𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏 ) )

Proof

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