Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lindssnlvec Structured version   Unicode version

Theorem lindssnlvec 38579
 Description: A singleton not containing the zero element of a vector space is always linearly independent. (Contributed by AV, 16-Apr-2019.) (Revised by AV, 28-Apr-2019.)
Assertion
Ref Expression
lindssnlvec linIndS

Proof of Theorem lindssnlvec
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eldifsni 4097 . . . . 5 Scalar Scalar Scalar
21adantl 464 . . . 4 Scalar Scalar Scalar
3 simpl3 1002 . . . 4 Scalar Scalar
4 eqid 2402 . . . . 5
5 eqid 2402 . . . . 5
6 eqid 2402 . . . . 5 Scalar Scalar
7 eqid 2402 . . . . 5 Scalar Scalar
8 eqid 2402 . . . . 5 Scalar Scalar
9 eqid 2402 . . . . 5
10 simpl1 1000 . . . . 5 Scalar Scalar
11 eldifi 3564 . . . . . 6 Scalar Scalar Scalar
1211adantl 464 . . . . 5 Scalar Scalar Scalar
13 simpl2 1001 . . . . 5 Scalar Scalar
144, 5, 6, 7, 8, 9, 10, 12, 13lvecvsn0 18073 . . . 4 Scalar Scalar Scalar
152, 3, 14mpbir2and 923 . . 3 Scalar Scalar
1615ralrimiva 2817 . 2 Scalar Scalar
17 lveclmod 18070 . . . . 5
1817anim1i 566 . . . 4