Definition df-lbs 21074

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

Assertion

Ref	Expression
df-lbs	⊢ LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})

Distinct variable group:   𝑛,𝑏,𝑠,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-lbs

Step	Hyp	Ref	Expression
1		clbs 21073	. 2 class LBasis
2		vw	. . 3 setvar 𝑤
3		cvv 3480	. . 3 class V
4		vb	. . . . . . . . . 10 setvar 𝑏
5	4	cv 1539	. . . . . . . . 9 class 𝑏
6		vn	. . . . . . . . . 10 setvar 𝑛
7	6	cv 1539	. . . . . . . . 9 class 𝑛
8	5, 7	cfv 6561	. . . . . . . 8 class (𝑛‘𝑏)
9	2	cv 1539	. . . . . . . . 9 class 𝑤
10		cbs 17247	. . . . . . . . 9 class Base
11	9, 10	cfv 6561	. . . . . . . 8 class (Base‘𝑤)
12	8, 11	wceq 1540	. . . . . . 7 wff (𝑛‘𝑏) = (Base‘𝑤)
13		vy	. . . . . . . . . . . . 13 setvar 𝑦
14	13	cv 1539	. . . . . . . . . . . 12 class 𝑦
15		vx	. . . . . . . . . . . . 13 setvar 𝑥
16	15	cv 1539	. . . . . . . . . . . 12 class 𝑥
17		cvsca 17301	. . . . . . . . . . . . 13 class ·𝑠
18	9, 17	cfv 6561	. . . . . . . . . . . 12 class ( ·𝑠 ‘𝑤)
19	14, 16, 18	co 7431	. . . . . . . . . . 11 class (𝑦( ·𝑠 ‘𝑤)𝑥)
20	16	csn 4626	. . . . . . . . . . . . 13 class {𝑥}
21	5, 20	cdif 3948	. . . . . . . . . . . 12 class (𝑏 ∖ {𝑥})
22	21, 7	cfv 6561	. . . . . . . . . . 11 class (𝑛‘(𝑏 ∖ {𝑥}))
23	19, 22	wcel 2108	. . . . . . . . . 10 wff (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
24	23	wn 3	. . . . . . . . 9 wff ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
25		vs	. . . . . . . . . . . 12 setvar 𝑠
26	25	cv 1539	. . . . . . . . . . 11 class 𝑠
27	26, 10	cfv 6561	. . . . . . . . . 10 class (Base‘𝑠)
28		c0g 17484	. . . . . . . . . . . 12 class 0g
29	26, 28	cfv 6561	. . . . . . . . . . 11 class (0g‘𝑠)
30	29	csn 4626	. . . . . . . . . 10 class {(0g‘𝑠)}
31	27, 30	cdif 3948	. . . . . . . . 9 class ((Base‘𝑠) ∖ {(0g‘𝑠)})
32	24, 13, 31	wral 3061	. . . . . . . 8 wff ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
33	32, 15, 5	wral 3061	. . . . . . 7 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
34	12, 33	wa 395	. . . . . 6 wff ((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
35		csca 17300	. . . . . . 7 class Scalar
36	9, 35	cfv 6561	. . . . . 6 class (Scalar‘𝑤)
37	34, 25, 36	wsbc 3788	. . . . 5 wff [(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
38		clspn 20969	. . . . . 6 class LSpan
39	9, 38	cfv 6561	. . . . 5 class (LSpan‘𝑤)
40	37, 6, 39	wsbc 3788	. . . 4 wff [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
41	11	cpw 4600	. . . 4 class 𝒫 (Base‘𝑤)
42	40, 4, 41	crab 3436	. . 3 class {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}
43	2, 3, 42	cmpt 5225	. 2 class (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
44	1, 43	wceq 1540	1 wff LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})

This definition is referenced by:  islbs  21075