Detailed syntax breakdown of Definition df-ssp
Step | Hyp | Ref
| Expression |
1 | | css 28648 |
. 2
class
SubSp |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | cnv 28511 |
. . 3
class
NrmCVec |
4 | | vw |
. . . . . . . 8
setvar 𝑤 |
5 | 4 | cv 1541 |
. . . . . . 7
class 𝑤 |
6 | | cpv 28512 |
. . . . . . 7
class
+𝑣 |
7 | 5, 6 | cfv 6333 |
. . . . . 6
class (
+𝑣 ‘𝑤) |
8 | 2 | cv 1541 |
. . . . . . 7
class 𝑢 |
9 | 8, 6 | cfv 6333 |
. . . . . 6
class (
+𝑣 ‘𝑢) |
10 | 7, 9 | wss 3841 |
. . . . 5
wff (
+𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) |
11 | | cns 28514 |
. . . . . . 7
class
·𝑠OLD |
12 | 5, 11 | cfv 6333 |
. . . . . 6
class (
·𝑠OLD ‘𝑤) |
13 | 8, 11 | cfv 6333 |
. . . . . 6
class (
·𝑠OLD ‘𝑢) |
14 | 12, 13 | wss 3841 |
. . . . 5
wff (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) |
15 | | cnmcv 28517 |
. . . . . . 7
class
normCV |
16 | 5, 15 | cfv 6333 |
. . . . . 6
class
(normCV‘𝑤) |
17 | 8, 15 | cfv 6333 |
. . . . . 6
class
(normCV‘𝑢) |
18 | 16, 17 | wss 3841 |
. . . . 5
wff
(normCV‘𝑤) ⊆ (normCV‘𝑢) |
19 | 10, 14, 18 | w3a 1088 |
. . . 4
wff ((
+𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢)) |
20 | 19, 4, 3 | crab 3057 |
. . 3
class {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢))} |
21 | 2, 3, 20 | cmpt 5107 |
. 2
class (𝑢 ∈ NrmCVec ↦ {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢))}) |
22 | 1, 21 | wceq 1542 |
1
wff SubSp =
(𝑢 ∈ NrmCVec ↦
{𝑤 ∈ NrmCVec ∣
(( +𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢))}) |