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	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lindfind.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lindfind.l	$$⊢L=\mathrm{Scalar}\left(W\right)$$
	lindfind.z	$$⊢\underset{\dot{}}{0}=0_L$$
	lindfind.k	$$⊢K={\mathrm{Base}}_L$$
Assertion	lindsind	$$⊢\left(\left(F\in \mathrm{LIndS}\left(W\right)\wedge E\in F\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lindfind.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
2		lindfind.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lindfind.l	$$⊢L=\mathrm{Scalar}\left(W\right)$$
4		lindfind.z	$$⊢\underset{\dot{}}{0}=0_L$$
5		lindfind.k	$$⊢K={\mathrm{Base}}_L$$
6		simplr	$$⊢\left(\left(F\in \mathrm{LIndS}\left(W\right)\wedge E\in F\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to E\in F$$
7		eldifsn	$$⊢A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)$$
8	7	biimpri	$$⊢\left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\to A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9	8	adantl	$$⊢\left(\left(F\in \mathrm{LIndS}\left(W\right)\wedge E\in F\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
10		elfvdm	$$⊢F\in \mathrm{LIndS}\left(W\right)\to W\in \mathrm{dom}\mathrm{LIndS}$$
11		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
12	11 1 2 3 5 4	islinds2	$$⊢W\in \mathrm{dom}\mathrm{LIndS}\to \left(F\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(F\subseteq {\mathrm{Base}}_W\wedge \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\right)\right)$$
13	10 12	syl	$$⊢F\in \mathrm{LIndS}\left(W\right)\to \left(F\in \mathrm{LIndS}\left(W\right)\leftrightarrow \left(F\subseteq {\mathrm{Base}}_W\wedge \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\right)\right)$$
14	13	ibi	$$⊢F\in \mathrm{LIndS}\left(W\right)\to \left(F\subseteq {\mathrm{Base}}_W\wedge \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\right)$$
15	14	simprd	$$⊢F\in \mathrm{LIndS}\left(W\right)\to \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)$$
16	15	ad2antrr	$$⊢\left(\left(F\in \mathrm{LIndS}\left(W\right)\wedge E\in F\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)$$
17		oveq2	$$⊢e=E\to a\underset{\dot{}}{·}e=a\underset{\dot{}}{·}E$$
18		sneq	$$⊢e=E\to \left\{e\right\}=\left\{E\right\}$$
19	18	difeq2d	$$⊢e=E\to F\setminus \left\{e\right\}=F\setminus \left\{E\right\}$$
20	19	fveq2d	$$⊢e=E\to N\left(F\setminus \left\{e\right\}\right)=N\left(F\setminus \left\{E\right\}\right)$$
21	17 20	eleq12d	$$⊢e=E\to \left(a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\leftrightarrow a\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\right)$$
22	21	notbid	$$⊢e=E\to \left(\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\leftrightarrow \neg a\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\right)$$
23		oveq1	$$⊢a=A\to a\underset{\dot{}}{·}E=A\underset{\dot{}}{·}E$$
24	23	eleq1d	$$⊢a=A\to \left(a\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\leftrightarrow A\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\right)$$
25	24	notbid	$$⊢a=A\to \left(\neg a\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\leftrightarrow \neg A\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)\right)$$
26	22 25	rspc2va	$$⊢\left(\left(E\in F\wedge A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\wedge \forall e\in F\forall a\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg a\underset{\dot{}}{·}e\in N\left(F\setminus \left\{e\right\}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)$$
27	6 9 16 26	syl21anc	$$⊢\left(\left(F\in \mathrm{LIndS}\left(W\right)\wedge E\in F\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(F\setminus \left\{E\right\}\right)$$