Detailed syntax breakdown of Definition df-lbs
Step | Hyp | Ref
| Expression |
1 | | clbs 20111 |
. 2
class
LBasis |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vb |
. . . . . . . . . 10
setvar 𝑏 |
5 | 4 | cv 1542 |
. . . . . . . . 9
class 𝑏 |
6 | | vn |
. . . . . . . . . 10
setvar 𝑛 |
7 | 6 | cv 1542 |
. . . . . . . . 9
class 𝑛 |
8 | 5, 7 | cfv 6380 |
. . . . . . . 8
class (𝑛‘𝑏) |
9 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑤 |
10 | | cbs 16760 |
. . . . . . . . 9
class
Base |
11 | 9, 10 | cfv 6380 |
. . . . . . . 8
class
(Base‘𝑤) |
12 | 8, 11 | wceq 1543 |
. . . . . . 7
wff (𝑛‘𝑏) = (Base‘𝑤) |
13 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
14 | 13 | cv 1542 |
. . . . . . . . . . . 12
class 𝑦 |
15 | | vx |
. . . . . . . . . . . . 13
setvar 𝑥 |
16 | 15 | cv 1542 |
. . . . . . . . . . . 12
class 𝑥 |
17 | | cvsca 16806 |
. . . . . . . . . . . . 13
class
·𝑠 |
18 | 9, 17 | cfv 6380 |
. . . . . . . . . . . 12
class (
·𝑠 ‘𝑤) |
19 | 14, 16, 18 | co 7213 |
. . . . . . . . . . 11
class (𝑦(
·𝑠 ‘𝑤)𝑥) |
20 | 16 | csn 4541 |
. . . . . . . . . . . . 13
class {𝑥} |
21 | 5, 20 | cdif 3863 |
. . . . . . . . . . . 12
class (𝑏 ∖ {𝑥}) |
22 | 21, 7 | cfv 6380 |
. . . . . . . . . . 11
class (𝑛‘(𝑏 ∖ {𝑥})) |
23 | 19, 22 | wcel 2110 |
. . . . . . . . . 10
wff (𝑦(
·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) |
24 | 23 | wn 3 |
. . . . . . . . 9
wff ¬
(𝑦(
·𝑠 ‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) |
25 | | vs |
. . . . . . . . . . . 12
setvar 𝑠 |
26 | 25 | cv 1542 |
. . . . . . . . . . 11
class 𝑠 |
27 | 26, 10 | cfv 6380 |
. . . . . . . . . 10
class
(Base‘𝑠) |
28 | | c0g 16944 |
. . . . . . . . . . . 12
class
0g |
29 | 26, 28 | cfv 6380 |
. . . . . . . . . . 11
class
(0g‘𝑠) |
30 | 29 | csn 4541 |
. . . . . . . . . 10
class
{(0g‘𝑠)} |
31 | 27, 30 | cdif 3863 |
. . . . . . . . 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 399 |
. . . . . 6
wff ((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) |
35 | | csca 16805 |
. . . . . . 7
class
Scalar |
36 | 9, 35 | cfv 6380 |
. . . . . 6
class
(Scalar‘𝑤) |
37 | 34, 25, 36 | wsbc 3694 |
. . . . 5
wff
[(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) |
38 | | clspn 20008 |
. . . . . 6
class
LSpan |
39 | 9, 38 | cfv 6380 |
. . . . 5
class
(LSpan‘𝑤) |
40 | 37, 6, 39 | wsbc 3694 |
. . . 4
wff
[(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) |
41 | 11 | cpw 4513 |
. . . 4
class 𝒫
(Base‘𝑤) |
42 | 40, 4, 41 | crab 3065 |
. . 3
class {𝑏 ∈ 𝒫
(Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} |
43 | 2, 3, 42 | cmpt 5135 |
. 2
class (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫
(Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) |
44 | 1, 43 | wceq 1543 |
1
wff LBasis =
(𝑤 ∈ V ↦ {𝑏 ∈ 𝒫
(Base‘𝑤) ∣
[(LSpan‘𝑤) /
𝑛][(Scalar‘𝑤) / 𝑠]((𝑛‘𝑏) = (Base‘𝑤) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ ((Base‘𝑠) ∖ {(0g‘𝑠)}) ¬ (𝑦( ·𝑠
‘𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}) |