Metamath Proof Explorer


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 LBasis = w V b 𝒫 Base w | [˙ LSpan w / n]˙ [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clbs class LBasis
1 vw setvar w
2 cvv class V
3 vb setvar b
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 clspn class LSpan
9 5 8 cfv class LSpan w
10 vn setvar n
11 csca class Scalar
12 5 11 cfv class Scalar w
13 vs setvar s
14 10 cv setvar n
15 3 cv setvar b
16 15 14 cfv class n b
17 16 6 wceq wff n b = Base w
18 vx setvar x
19 vy setvar y
20 13 cv setvar s
21 20 4 cfv class Base s
22 c0g class 0 𝑔
23 20 22 cfv class 0 s
24 23 csn class 0 s
25 21 24 cdif class Base s 0 s
26 19 cv setvar y
27 cvsca class 𝑠
28 5 27 cfv class w
29 18 cv setvar x
30 26 29 28 co class y w x
31 29 csn class x
32 15 31 cdif class b x
33 32 14 cfv class n b x
34 30 33 wcel wff y w x n b x
35 34 wn wff ¬ y w x n b x
36 35 19 25 wral wff y Base s 0 s ¬ y w x n b x
37 36 18 15 wral wff x b y Base s 0 s ¬ y w x n b x
38 17 37 wa wff n b = Base w x b y Base s 0 s ¬ y w x n b x
39 38 13 12 wsbc wff [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x
40 39 10 9 wsbc wff [˙ LSpan w / n]˙ [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x
41 40 3 7 crab class b 𝒫 Base w | [˙ LSpan w / n]˙ [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x
42 1 2 41 cmpt class w V b 𝒫 Base w | [˙ LSpan w / n]˙ [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x
43 0 42 wceq wff LBasis = w V b 𝒫 Base w | [˙ LSpan w / n]˙ [˙ Scalar w / s]˙ n b = Base w x b y Base s 0 s ¬ y w x n b x