Theorem lbslinds

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

	Ref	Expression
Hypothesis	lbslinds.j	|- J = ( LBasis ` W )
Assertion	lbslinds	|- J C_ ( LIndS ` W )

Proof

Step	Hyp	Ref	Expression
1		lbslinds.j	|- J = ( LBasis ` W )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3		eqid	|- ( LSpan ` W ) = ( LSpan ` W )
4	2 1 3	islbs4	|- ( a e. J <-> ( a e. ( LIndS ` W ) /\ ( ( LSpan ` W ) ` a ) = ( Base ` W ) ) )
5	4	simplbi	|- ( a e. J -> a e. ( LIndS ` W ) )
6	5	ssriv	|- J C_ ( LIndS ` W )