Metamath Proof Explorer


Theorem lbslinds

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

Ref Expression
Hypothesis lbslinds.j J=LBasisW
Assertion lbslinds JLIndSW

Proof

Step Hyp Ref Expression
1 lbslinds.j J=LBasisW
2 eqid BaseW=BaseW
3 eqid LSpanW=LSpanW
4 2 1 3 islbs4 aJaLIndSWLSpanWa=BaseW
5 4 simplbi aJaLIndSW
6 5 ssriv JLIndSW