Metamath Proof Explorer

Theorem lindfind

Description: A linearly independent family is independent: no nonzero element multiple can be expressed as a linear combination of the others. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses lindfind.s ⊢·˙=⋅W
lindfind.n ⊢N=LSpan⁡W
lindfind.l ⊢L=Scalar⁡W
lindfind.z ⊢0˙=0L
lindfind.k ⊢K=BaseL
Assertion lindfind ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→¬A·˙F⁡E∈N⁡Fdom⁡F∖E

Proof

Step Hyp Ref Expression
1 lindfind.s ⊢·˙=⋅W
2 lindfind.n ⊢N=LSpan⁡W
3 lindfind.l ⊢L=Scalar⁡W
4 lindfind.z ⊢0˙=0L
5 lindfind.k ⊢K=BaseL
6 simplr ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→E∈dom⁡F
7 eldifsn ⊢A∈K∖0˙↔A∈K∧A≠0˙
8 7 biimpri ⊢A∈K∧A≠0˙→A∈K∖0˙
9 8 adantl ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→A∈K∖0˙
10 simpll ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→FLIndFW
11 3 5 elbasfv ⊢A∈K→W∈V
12 11 ad2antrl ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→W∈V
13 rellindf ⊢Rel⁡LIndF
14 13 brrelex1i ⊢FLIndFW→F∈V
15 14 ad2antrr ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→F∈V
16 eqid ⊢BaseW=BaseW
17 16 1 2 3 5 4 islindf ⊢W∈V∧F∈V→FLIndFW↔F:dom⁡F⟶BaseW∧∀e∈dom⁡F∀a∈K∖0˙¬a·˙F⁡e∈N⁡Fdom⁡F∖e
18 12 15 17 syl2anc ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→FLIndFW↔F:dom⁡F⟶BaseW∧∀e∈dom⁡F∀a∈K∖0˙¬a·˙F⁡e∈N⁡Fdom⁡F∖e
19 10 18 mpbid ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→F:dom⁡F⟶BaseW∧∀e∈dom⁡F∀a∈K∖0˙¬a·˙F⁡e∈N⁡Fdom⁡F∖e
20 19 simprd ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→∀e∈dom⁡F∀a∈K∖0˙¬a·˙F⁡e∈N⁡Fdom⁡F∖e
21 fveq2 ⊢e=E→F⁡e=F⁡E
22 21 oveq2d ⊢e=E→a·˙F⁡e=a·˙F⁡E
23 sneq ⊢e=E→e=E
24 23 difeq2d ⊢e=E→dom⁡F∖e=dom⁡F∖E
25 24 imaeq2d ⊢e=E→Fdom⁡F∖e=Fdom⁡F∖E
26 25 fveq2d ⊢e=E→N⁡Fdom⁡F∖e=N⁡Fdom⁡F∖E
27 22 26 eleq12d ⊢e=E→a·˙F⁡e∈N⁡Fdom⁡F∖e↔a·˙F⁡E∈N⁡Fdom⁡F∖E
28 27 notbid ⊢e=E→¬a·˙F⁡e∈N⁡Fdom⁡F∖e↔¬a·˙F⁡E∈N⁡Fdom⁡F∖E
29 oveq1 ⊢a=A→a·˙F⁡E=A·˙F⁡E
30 29 eleq1d ⊢a=A→a·˙F⁡E∈N⁡Fdom⁡F∖E↔A·˙F⁡E∈N⁡Fdom⁡F∖E
31 30 notbid ⊢a=A→¬a·˙F⁡E∈N⁡Fdom⁡F∖E↔¬A·˙F⁡E∈N⁡Fdom⁡F∖E
32 28 31 rspc2va ⊢E∈dom⁡F∧A∈K∖0˙∧∀e∈dom⁡F∀a∈K∖0˙¬a·˙F⁡e∈N⁡Fdom⁡F∖e→¬A·˙F⁡E∈N⁡Fdom⁡F∖E
33 6 9 20 32 syl21anc ⊢FLIndFW∧E∈dom⁡F∧A∈K∧A≠0˙→¬A·˙F⁡E∈N⁡Fdom⁡F∖E