Theorem lbsind

Description: A basis is linearly independent; that is, every element has a span which trivially intersects the span of the remainder of the basis. (Contributed by Mario Carneiro, 12-Jan-2015)

	Ref	Expression
Hypotheses	lbsss.v	$$⊢V={\mathrm{Base}}_W$$
	lbsss.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	lbssp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lbsind.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lbsind.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lbsind.k	$$⊢K={\mathrm{Base}}_F$$
	lbsind.z	$$⊢\underset{\dot{}}{0}=0_F$$
Assertion	lbsind	$$⊢\left(\left(B\in J\wedge E\in B\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lbsss.v	$$⊢V={\mathrm{Base}}_W$$
2		lbsss.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
3		lbssp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lbsind.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		lbsind.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		lbsind.k	$$⊢K={\mathrm{Base}}_F$$
7		lbsind.z	$$⊢\underset{\dot{}}{0}=0_F$$
8		eldifsn	$$⊢A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)$$
9		elfvdm	$$⊢B\in \mathrm{LBasis}\left(W\right)\to W\in \mathrm{dom}\mathrm{LBasis}$$
10	9 2	eleq2s	$$⊢B\in J\to W\in \mathrm{dom}\mathrm{LBasis}$$
11	1 4 5 6 2 3 7	islbs	$$⊢W\in \mathrm{dom}\mathrm{LBasis}\to \left(B\in J\leftrightarrow \left(B\subseteq V\wedge N\left(B\right)=V\wedge \forall x\in B\forall y\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\right)\right)$$
12	10 11	syl	$$⊢B\in J\to \left(B\in J\leftrightarrow \left(B\subseteq V\wedge N\left(B\right)=V\wedge \forall x\in B\forall y\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\right)\right)$$
13	12	ibi	$$⊢B\in J\to \left(B\subseteq V\wedge N\left(B\right)=V\wedge \forall x\in B\forall y\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\right)$$
14	13	simp3d	$$⊢B\in J\to \forall x\in B\forall y\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)$$
15		oveq2	$$⊢x=E\to y\underset{\dot{}}{·}x=y\underset{\dot{}}{·}E$$
16		sneq	$$⊢x=E\to \left\{x\right\}=\left\{E\right\}$$
17	16	difeq2d	$$⊢x=E\to B\setminus \left\{x\right\}=B\setminus \left\{E\right\}$$
18	17	fveq2d	$$⊢x=E\to N\left(B\setminus \left\{x\right\}\right)=N\left(B\setminus \left\{E\right\}\right)$$
19	15 18	eleq12d	$$⊢x=E\to \left(y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\leftrightarrow y\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
20	19	notbid	$$⊢x=E\to \left(\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\leftrightarrow \neg y\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
21		oveq1	$$⊢y=A\to y\underset{\dot{}}{·}E=A\underset{\dot{}}{·}E$$
22	21	eleq1d	$$⊢y=A\to \left(y\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\leftrightarrow A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
23	22	notbid	$$⊢y=A\to \left(\neg y\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\leftrightarrow \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
24	20 23	rspc2v	$$⊢\left(E\in B\wedge A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\forall x\in B\forall y\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\neg y\underset{\dot{}}{·}x\in N\left(B\setminus \left\{x\right\}\right)\to \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
25	14 24	syl5com	$$⊢B\in J\to \left(\left(E\in B\wedge A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)\right)$$
26	25	impl	$$⊢\left(\left(B\in J\wedge E\in B\right)\wedge A\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)$$
27	8 26	sylan2br	$$⊢\left(\left(B\in J\wedge E\in B\right)\wedge \left(A\in K\wedge A\ne \underset{\dot{}}{0}\right)\right)\to \neg A\underset{\dot{}}{·}E\in N\left(B\setminus \left\{E\right\}\right)$$