Theorem lbsext

Description: For any linearly independent subset C of V , there is a basis containing the vectors in C . (Contributed by Mario Carneiro, 25-Jun-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypotheses	lbsex.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
	lbsex.v	$$⊢V={\mathrm{Base}}_W$$
	lbsex.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
Assertion	lbsext	$$⊢\left(W\in \mathrm{LVec}\wedge C\subseteq V\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)\to \exists s\in JC\subseteq s$$

Proof

Step	Hyp	Ref	Expression
1		lbsex.j	$$⊢J=\mathrm{LBasis}\left(W\right)$$
2		lbsex.v	$$⊢V={\mathrm{Base}}_W$$
3		lbsex.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4	2	fvexi	$$⊢V\in \mathrm{V}$$
5	4	pwex	$$⊢𝒫V\in \mathrm{V}$$
6		numth3	$$⊢𝒫V\in \mathrm{V}\to 𝒫V\in \mathrm{dom}\mathrm{card}$$
7	5 6	ax-mp	$$⊢𝒫V\in \mathrm{dom}\mathrm{card}$$
8	7	jctr	$$⊢W\in \mathrm{LVec}\to \left(W\in \mathrm{LVec}\wedge 𝒫V\in \mathrm{dom}\mathrm{card}\right)$$
9	1 2 3	lbsextg	$$⊢\left(\left(W\in \mathrm{LVec}\wedge 𝒫V\in \mathrm{dom}\mathrm{card}\right)\wedge C\subseteq V\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)\to \exists s\in JC\subseteq s$$
10	8 9	syl3an1	$$⊢\left(W\in \mathrm{LVec}\wedge C\subseteq V\wedge \forall x\in C\neg x\in N\left(C\setminus \left\{x\right\}\right)\right)\to \exists s\in JC\subseteq s$$