Metamath Proof Explorer

Definition df-lss

Description: Define the set of linear subspaces of a left module or left vector space: a linear subspace of a left module or left vector space is a non-empty subset of the base set of the left module/vector space with a closure condition on vector addition and scalar multiplication. (Contributed by NM, 8-Dec-2013)

Ref Expression
Assertion df-lss ⊢ LSubSp = w ∈ V ⟼ s ∈ 𝒫 Base w ∖ ∅ | ∀ x ∈ Base Scalar ⁡ w ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 clss class LSubSp
1 vw setvar w
2 cvv class V
3 vs setvar s
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 6 cpw class 𝒫 Base w
8 c0 class ∅
9 8 csn class ∅
10 7 9 cdif class 𝒫 Base w ∖ ∅
11 vx setvar x
12 csca class Scalar
13 5 12 cfv class Scalar ⁡ w
14 13 4 cfv class Base Scalar ⁡ w
15 va setvar a
16 3 cv setvar s
17 vb setvar b
18 11 cv setvar x
19 cvsca class ⋅ 𝑠
20 5 19 cfv class ⋅ w
21 15 cv setvar a
22 18 21 20 co class x ⋅ w a
23 cplusg class + 𝑔
24 5 23 cfv class + w
25 17 cv setvar b
26 22 25 24 co class x ⋅ w a + w b
27 26 16 wcel wff x ⋅ w a + w b ∈ s
28 27 17 16 wral wff ∀ b ∈ s x ⋅ w a + w b ∈ s
29 28 15 16 wral wff ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s
30 29 11 14 wral wff ∀ x ∈ Base Scalar ⁡ w ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s
31 30 3 10 crab class s ∈ 𝒫 Base w ∖ ∅ | ∀ x ∈ Base Scalar ⁡ w ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s
32 1 2 31 cmpt class w ∈ V ⟼ s ∈ 𝒫 Base w ∖ ∅ | ∀ x ∈ Base Scalar ⁡ w ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s
33 0 32 wceq wff LSubSp = w ∈ V ⟼ s ∈ 𝒫 Base w ∖ ∅ | ∀ x ∈ Base Scalar ⁡ w ∀ a ∈ s ∀ b ∈ s x ⋅ w a + w b ∈ s