Theorem lbsind2

Description: A basis is linearly independent; that is, every element is not in the span of the remainder of the basis. (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 12-Jan-2015)

	Ref	Expression
Hypotheses	lbsind2.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	lbsind2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lbsind2.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lbsind2.o	$$⊢\underset{\dot{}}{1}=1_F$$
	lbsind2.z	$$⊢\underset{\dot{}}{0}=0_F$$
Assertion	lbsind2	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \neg E\in N\left(B\setminus \left\{E\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lbsind2.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
2		lbsind2.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lbsind2.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		lbsind2.o	$$⊢\underset{\dot{}}{1}=1_F$$
5		lbsind2.z	$$⊢\underset{\dot{}}{0}=0_F$$
6		simp1l	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to W\in \mathrm{LMod}$$
7		simp2	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to B\in J$$
8		simp3	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to E\in B$$
9		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
10	9 1	lbsel	$$⊢\left(B\in J\wedge E\in B\right)\to E\in {\mathrm{Base}}_W$$
11	7 8 10	syl2anc	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to E\in {\mathrm{Base}}_W$$
12		eqid	$$⊢{\cdot }_W={\cdot }_W$$
13	9 3 12 4	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge E\in {\mathrm{Base}}_W\right)\to \underset{\dot{}}{1}{\cdot }_{W}E=E$$
14	6 11 13	syl2anc	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \underset{\dot{}}{1}{\cdot }_{W}E=E$$
15	3	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
16		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
17	16 4	ringidcl	$$⊢F\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
18	6 15 17	3syl	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_F$$
19		simp1r	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
20	9 1 2 3 12 16 5	lbsind	$$⊢\left(\left(B\in J\wedge E\in B\right)\wedge \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_F\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\right)\to \neg \underset{\dot{}}{1}{\cdot }_{W}E\in N\left(B\setminus \left\{E\right\}\right)$$
21	7 8 18 19 20	syl22anc	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \neg \underset{\dot{}}{1}{\cdot }_{W}E\in N\left(B\setminus \left\{E\right\}\right)$$
22	14 21	eqneltrrd	$$⊢\left(\left(W\in \mathrm{LMod}\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\wedge B\in J\wedge E\in B\right)\to \neg E\in N\left(B\setminus \left\{E\right\}\right)$$