Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lindsind Structured version   Unicode version

Theorem lindsind 27278
 Description: A linearly independent set is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Hypotheses
Ref Expression
lindfind.s
lindfind.n
lindfind.l Scalar
lindfind.z
lindfind.k
Assertion
Ref Expression
lindsind LIndS

Proof of Theorem lindsind
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 733 . 2 LIndS
2 eldifsn 3929 . . . 4
32biimpri 199 . . 3
5 elfvdm 5760 . . . . . 6 LIndS LIndS
6 eqid 2438 . . . . . . 7
7 lindfind.s . . . . . . 7
8 lindfind.n . . . . . . 7
9 lindfind.l . . . . . . 7 Scalar
10 lindfind.k . . . . . . 7
11 lindfind.z . . . . . . 7
126, 7, 8, 9, 10, 11islinds2 27274 . . . . . 6 LIndS LIndS
135, 12syl 16 . . . . 5 LIndS LIndS
1413ibi 234 . . . 4 LIndS
1514simprd 451 . . 3 LIndS