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 ‘ 𝑊 ) ↔ ∃ 𝑏 ∈ 𝐽 𝑌 ⊆ 𝑏 ) )