Theorem lbslinds

Description: A basis is independent. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Hypothesis	lbslinds.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
Assertion	lbslinds	⊢ 𝐽 ⊆ ( LIndS ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		lbslinds.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
2		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
3		eqid	⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
4	2 1 3	islbs4	⊢ ( 𝑎 ∈ 𝐽 ↔ ( 𝑎 ∈ ( LIndS ‘ 𝑊 ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ 𝑎 ) = ( Base ‘ 𝑊 ) ) )
5	4	simplbi	⊢ ( 𝑎 ∈ 𝐽 → 𝑎 ∈ ( LIndS ‘ 𝑊 ) )
6	5	ssriv	⊢ 𝐽 ⊆ ( LIndS ‘ 𝑊 )