Detailed syntax breakdown of Definition df-lss
Step | Hyp | Ref
| Expression |
1 | | clss 20202 |
. 2
class
LSubSp |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3433 |
. . 3
class
V |
4 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
5 | 4 | cv 1538 |
. . . . . . . . . 10
class 𝑥 |
6 | | va |
. . . . . . . . . . 11
setvar 𝑎 |
7 | 6 | cv 1538 |
. . . . . . . . . 10
class 𝑎 |
8 | 2 | cv 1538 |
. . . . . . . . . . 11
class 𝑤 |
9 | | cvsca 16975 |
. . . . . . . . . . 11
class
·𝑠 |
10 | 8, 9 | cfv 6437 |
. . . . . . . . . 10
class (
·𝑠 ‘𝑤) |
11 | 5, 7, 10 | co 7284 |
. . . . . . . . 9
class (𝑥(
·𝑠 ‘𝑤)𝑎) |
12 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
13 | 12 | cv 1538 |
. . . . . . . . 9
class 𝑏 |
14 | | cplusg 16971 |
. . . . . . . . . 10
class
+g |
15 | 8, 14 | cfv 6437 |
. . . . . . . . 9
class
(+g‘𝑤) |
16 | 11, 13, 15 | co 7284 |
. . . . . . . 8
class ((𝑥(
·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) |
17 | | vs |
. . . . . . . . 9
setvar 𝑠 |
18 | 17 | cv 1538 |
. . . . . . . 8
class 𝑠 |
19 | 16, 18 | wcel 2107 |
. . . . . . 7
wff ((𝑥(
·𝑠 ‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 |
20 | 19, 12, 18 | wral 3065 |
. . . . . 6
wff
∀𝑏 ∈
𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 |
21 | 20, 6, 18 | wral 3065 |
. . . . 5
wff
∀𝑎 ∈
𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 |
22 | | csca 16974 |
. . . . . . 7
class
Scalar |
23 | 8, 22 | cfv 6437 |
. . . . . 6
class
(Scalar‘𝑤) |
24 | | cbs 16921 |
. . . . . 6
class
Base |
25 | 23, 24 | cfv 6437 |
. . . . 5
class
(Base‘(Scalar‘𝑤)) |
26 | 21, 4, 25 | wral 3065 |
. . . 4
wff
∀𝑥 ∈
(Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠 |
27 | 8, 24 | cfv 6437 |
. . . . . 6
class
(Base‘𝑤) |
28 | 27 | cpw 4534 |
. . . . 5
class 𝒫
(Base‘𝑤) |
29 | | c0 4257 |
. . . . . 6
class
∅ |
30 | 29 | csn 4562 |
. . . . 5
class
{∅} |
31 | 28, 30 | cdif 3885 |
. . . 4
class
(𝒫 (Base‘𝑤) ∖ {∅}) |
32 | 26, 17, 31 | crab 3069 |
. . 3
class {𝑠 ∈ (𝒫
(Base‘𝑤) ∖
{∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠} |
33 | 2, 3, 32 | cmpt 5158 |
. 2
class (𝑤 ∈ V ↦ {𝑠 ∈ (𝒫
(Base‘𝑤) ∖
{∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠}) |
34 | 1, 33 | wceq 1539 |
1
wff LSubSp =
(𝑤 ∈ V ↦ {𝑠 ∈ (𝒫
(Base‘𝑤) ∖
{∅}) ∣ ∀𝑥 ∈ (Base‘(Scalar‘𝑤))∀𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ((𝑥( ·𝑠
‘𝑤)𝑎)(+g‘𝑤)𝑏) ∈ 𝑠}) |