Definition df-lbs

Description: Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Assertion	df-lbs	$$⊢\mathrm{LBasis}=\left(w\in \mathrm{V}⟼\left\{b\in 𝒫{\mathrm{Base}}_w|\underset{\dot{}}{[}\mathrm{LSpan}\left(w\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clbs	$$class\mathrm{LBasis}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vb	$$setvarb$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7	6	cpw	$$class𝒫{\mathrm{Base}}_w$$
8		clspn	$$class\mathrm{LSpan}$$
9	5 8	cfv	$$class\mathrm{LSpan}\left(w\right)$$
10		vn	$$setvarn$$
11		csca	$$class\mathrm{Scalar}$$
12	5 11	cfv	$$class\mathrm{Scalar}\left(w\right)$$
13		vs	$$setvars$$
14	10	cv	$$setvarn$$
15	3	cv	$$setvarb$$
16	15 14	cfv	$$classn\left(b\right)$$
17	16 6	wceq	$$wffn\left(b\right)={\mathrm{Base}}_w$$
18		vx	$$setvarx$$
19		vy	$$setvary$$
20	13	cv	$$setvars$$
21	20 4	cfv	$$class{\mathrm{Base}}_s$$
22		c0g	$$class{0}_{𝑔}$$
23	20 22	cfv	$$class{0}_s$$
24	23	csn	$$class\left\{0_s\right\}$$
25	21 24	cdif	$$class\left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)$$
26	19	cv	$$setvary$$
27		cvsca	$$class{\cdot }_{𝑠}$$
28	5 27	cfv	$$class{\cdot }_w$$
29	18	cv	$$setvarx$$
30	26 29 28	co	$$class\left(y{\cdot }_{w}x\right)$$
31	29	csn	$$class\left\{x\right\}$$
32	15 31	cdif	$$class\left(b\setminus \left\{x\right\}\right)$$
33	32 14	cfv	$$classn\left(b\setminus \left\{x\right\}\right)$$
34	30 33	wcel	$$wffy{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)$$
35	34	wn	$$wff\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)$$
36	35 19 25	wral	$$wff\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)$$
37	36 18 15	wral	$$wff\forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)$$
38	17 37	wa	$$wff\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)$$
39	38 13 12	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)$$
40	39 10 9	wsbc	$$wff\underset{\dot{}}{[}\mathrm{LSpan}\left(w\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)$$
41	40 3 7	crab	$$class\left\{b\in 𝒫{\mathrm{Base}}_w|\underset{\dot{}}{[}\mathrm{LSpan}\left(w\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)\right\}$$
42	1 2 41	cmpt	$$class\left(w\in \mathrm{V}⟼\left\{b\in 𝒫{\mathrm{Base}}_w|\underset{\dot{}}{[}\mathrm{LSpan}\left(w\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)\right\}\right)$$
43	0 42	wceq	$$wff\mathrm{LBasis}=\left(w\in \mathrm{V}⟼\left\{b\in 𝒫{\mathrm{Base}}_w|\underset{\dot{}}{[}\mathrm{LSpan}\left(w\right)/n\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/s\underset{\dot{}}{]}\left(n\left(b\right)={\mathrm{Base}}_w\wedge \forall x\in b\forall y\in \left({\mathrm{Base}}_s\setminus \left\{0_s\right\}\right)\neg y{\cdot }_{w}x\in n\left(b\setminus \left\{x\right\}\right)\right)\right\}\right)$$