Metamath Proof Explorer


Theorem lindsind

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)

Ref Expression
Hypotheses lindfind.s · ˙ = W
lindfind.n N = LSpan W
lindfind.l L = Scalar W
lindfind.z 0 ˙ = 0 L
lindfind.k K = Base L
Assertion lindsind F LIndS W E F A K A 0 ˙ ¬ A · ˙ E N 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 ˙ = 0 L
5 lindfind.k K = Base L
6 simplr F LIndS W E F A K A 0 ˙ E F
7 eldifsn A K 0 ˙ A K A 0 ˙
8 7 biimpri A K A 0 ˙ A K 0 ˙
9 8 adantl F LIndS W E F A K A 0 ˙ A K 0 ˙
10 elfvdm F LIndS W W dom LIndS
11 eqid Base W = Base W
12 11 1 2 3 5 4 islinds2 W dom LIndS F LIndS W F Base W e F a K 0 ˙ ¬ a · ˙ e N F e
13 10 12 syl F LIndS W F LIndS W F Base W e F a K 0 ˙ ¬ a · ˙ e N F e
14 13 ibi F LIndS W F Base W e F a K 0 ˙ ¬ a · ˙ e N F e
15 14 simprd F LIndS W e F a K 0 ˙ ¬ a · ˙ e N F e
16 15 ad2antrr F LIndS W E F A K A 0 ˙ e F a K 0 ˙ ¬ a · ˙ e N F e
17 oveq2 e = E a · ˙ e = a · ˙ E
18 sneq e = E e = E
19 18 difeq2d e = E F e = F E
20 19 fveq2d e = E N F e = N F E
21 17 20 eleq12d e = E a · ˙ e N F e a · ˙ E N F E
22 21 notbid e = E ¬ a · ˙ e N F e ¬ a · ˙ E N F E
23 oveq1 a = A a · ˙ E = A · ˙ E
24 23 eleq1d a = A a · ˙ E N F E A · ˙ E N F E
25 24 notbid a = A ¬ a · ˙ E N F E ¬ A · ˙ E N F E
26 22 25 rspc2va E F A K 0 ˙ e F a K 0 ˙ ¬ a · ˙ e N F e ¬ A · ˙ E N F E
27 6 9 16 26 syl21anc F LIndS W E F A K A 0 ˙ ¬ A · ˙ E N F E