Theorem lbssp

Description: The span of a basis is the whole space. (Contributed by Mario Carneiro, 24-Jun-2014)

	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)$$
Assertion	lbssp	$$⊢B\in J\to N\left(B\right)=V$$

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		elfvdm	$$⊢B\in \mathrm{LBasis}\left(W\right)\to W\in \mathrm{dom}\mathrm{LBasis}$$
5	4 2	eleq2s	$$⊢B\in J\to W\in \mathrm{dom}\mathrm{LBasis}$$
6		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
7		eqid	$$⊢{\cdot }_W={\cdot }_W$$
8		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
9		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
10	1 6 7 8 2 3 9	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({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in N\left(B\setminus \left\{x\right\}\right)\right)\right)$$
11	5 10	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({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in N\left(B\setminus \left\{x\right\}\right)\right)\right)$$
12	11	ibi	$$⊢B\in J\to \left(B\subseteq V\wedge N\left(B\right)=V\wedge \forall x\in B\forall y\in \left({\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\setminus \left\{0_{\mathrm{Scalar}\left(W\right)}\right\}\right)\neg y{\cdot }_{W}x\in N\left(B\setminus \left\{x\right\}\right)\right)$$
13	12	simp2d	$$⊢B\in J\to N\left(B\right)=V$$