Definition df-lbs 21343

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 21342	. 2 class LBasis
2		vw	. . 3 setvar 𝑤
3		cvv 3451	. . 3 class V
4		vb	. . . . . . . . . 10 setvar 𝑏
5	4	cv 1569	. . . . . . . . 9 class 𝑏
6		vn	. . . . . . . . . 10 setvar 𝑛
7	6	cv 1569	. . . . . . . . 9 class 𝑛
8	5, 7	cfv 6537	. . . . . . . 8 class (𝑛‘𝑏)
9	2	cv 1569	. . . . . . . . 9 class 𝑤
10		cbs 17380	. . . . . . . . 9 class Base
11	9, 10	cfv 6537	. . . . . . . 8 class (Base‘𝑤)
12	8, 11	wceq 1570	. . . . . . 7 wff (𝑛‘𝑏) = (Base‘𝑤)
13		vy	. . . . . . . . . . . . 13 setvar 𝑦
14	13	cv 1569	. . . . . . . . . . . 12 class 𝑦
15		vx	. . . . . . . . . . . . 13 setvar 𝑥
16	15	cv 1569	. . . . . . . . . . . 12 class 𝑥
17		cvsca 17425	. . . . . . . . . . . . 13 class ·𝑠
18	9, 17	cfv 6537	. . . . . . . . . . . 12 class ( ·𝑠 ‘𝑤)
19	14, 16, 18	co 7418	. . . . . . . . . . 11 class (𝑦( ·𝑠 ‘𝑤)𝑥)
20	16	csn 4584	. . . . . . . . . . . . 13 class {𝑥}
21	5, 20	cdif 3896	. . . . . . . . . . . 12 class (𝑏 ∖ {𝑥})
22	21, 7	cfv 6537	. . . . . . . . . . 11 class (𝑛‘(𝑏 ∖ {𝑥}))
23	19, 22	wcel 2145	. . . . . . . . . 10 wff (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
24	23	wn 3	. . . . . . . . 9 wff ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
25		vs	. . . . . . . . . . . 12 setvar 𝑠
26	25	cv 1569	. . . . . . . . . . 11 class 𝑠
27	26, 10	cfv 6537	. . . . . . . . . 10 class (Base‘𝑠)
28		c0g 17603	. . . . . . . . . . . 12 class 0g
29	26, 28	cfv 6537	. . . . . . . . . . 11 class (0g‘𝑠)
30	29	csn 4584	. . . . . . . . . 10 class {(0g‘𝑠)}
31	27, 30	cdif 3896	. . . . . . . . 9 class ((Base‘𝑠) ∖ {(0g‘𝑠)})
32	24, 13, 31	wral 3077	. . . . . . . 8 wff ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
33	32, 15, 5	wral 3077	. . . . . . 7 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
34	12, 33	wa 401	. . . . . 6 wff ((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
35		csca 17424	. . . . . . 7 class Scalar
36	9, 35	cfv 6537	. . . . . 6 class (Scalar‘𝑤)
37	34, 25, 36	wsbc 3739	. . . . 5 wff [(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
38		clspn 21239	. . . . . 6 class LSpan
39	9, 38	cfv 6537	. . . . 5 class (LSpan‘𝑤)
40	37, 6, 39	wsbc 3739	. . . 4 wff [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
41	11	cpw 4557	. . . 4 class 𝒫 (Base‘𝑤)
42	40, 4, 41	crab 3413	. . 3 class {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}
43	2, 3, 42	cmpt 5186	. 2 class (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
44	1, 43	wceq 1570	1 wff LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})

This definition is used by:  islbs  21344