Detailed syntax breakdown of Definition df-nv
Step | Hyp | Ref
| Expression |
1 | | cnv 28511 |
. 2
class
NrmCVec |
2 | | vg |
. . . . . . 7
setvar 𝑔 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑔 |
4 | | vs |
. . . . . . 7
setvar 𝑠 |
5 | 4 | cv 1541 |
. . . . . 6
class 𝑠 |
6 | 3, 5 | cop 4519 |
. . . . 5
class
〈𝑔, 𝑠〉 |
7 | | cvc 28485 |
. . . . 5
class
CVecOLD |
8 | 6, 7 | wcel 2113 |
. . . 4
wff 〈𝑔, 𝑠〉 ∈
CVecOLD |
9 | 3 | crn 5520 |
. . . . 5
class ran 𝑔 |
10 | | cr 10607 |
. . . . 5
class
ℝ |
11 | | vn |
. . . . . 6
setvar 𝑛 |
12 | 11 | cv 1541 |
. . . . 5
class 𝑛 |
13 | 9, 10, 12 | wf 6329 |
. . . 4
wff 𝑛:ran 𝑔⟶ℝ |
14 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
15 | 14 | cv 1541 |
. . . . . . . . 9
class 𝑥 |
16 | 15, 12 | cfv 6333 |
. . . . . . . 8
class (𝑛‘𝑥) |
17 | | cc0 10608 |
. . . . . . . 8
class
0 |
18 | 16, 17 | wceq 1542 |
. . . . . . 7
wff (𝑛‘𝑥) = 0 |
19 | | cgi 28417 |
. . . . . . . . 9
class
GId |
20 | 3, 19 | cfv 6333 |
. . . . . . . 8
class
(GId‘𝑔) |
21 | 15, 20 | wceq 1542 |
. . . . . . 7
wff 𝑥 = (GId‘𝑔) |
22 | 18, 21 | wi 4 |
. . . . . 6
wff ((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) |
23 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
24 | 23 | cv 1541 |
. . . . . . . . . 10
class 𝑦 |
25 | 24, 15, 5 | co 7164 |
. . . . . . . . 9
class (𝑦𝑠𝑥) |
26 | 25, 12 | cfv 6333 |
. . . . . . . 8
class (𝑛‘(𝑦𝑠𝑥)) |
27 | | cabs 14676 |
. . . . . . . . . 10
class
abs |
28 | 24, 27 | cfv 6333 |
. . . . . . . . 9
class
(abs‘𝑦) |
29 | | cmul 10613 |
. . . . . . . . 9
class
· |
30 | 28, 16, 29 | co 7164 |
. . . . . . . 8
class
((abs‘𝑦)
· (𝑛‘𝑥)) |
31 | 26, 30 | wceq 1542 |
. . . . . . 7
wff (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) |
32 | | cc 10606 |
. . . . . . 7
class
ℂ |
33 | 31, 23, 32 | wral 3053 |
. . . . . 6
wff
∀𝑦 ∈
ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) |
34 | 15, 24, 3 | co 7164 |
. . . . . . . . 9
class (𝑥𝑔𝑦) |
35 | 34, 12 | cfv 6333 |
. . . . . . . 8
class (𝑛‘(𝑥𝑔𝑦)) |
36 | 24, 12 | cfv 6333 |
. . . . . . . . 9
class (𝑛‘𝑦) |
37 | | caddc 10611 |
. . . . . . . . 9
class
+ |
38 | 16, 36, 37 | co 7164 |
. . . . . . . 8
class ((𝑛‘𝑥) + (𝑛‘𝑦)) |
39 | | cle 10747 |
. . . . . . . 8
class
≤ |
40 | 35, 38, 39 | wbr 5027 |
. . . . . . 7
wff (𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)) |
41 | 40, 23, 9 | wral 3053 |
. . . . . 6
wff
∀𝑦 ∈ ran
𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)) |
42 | 22, 33, 41 | w3a 1088 |
. . . . 5
wff (((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))) |
43 | 42, 14, 9 | wral 3053 |
. . . 4
wff
∀𝑥 ∈ ran
𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))) |
44 | 8, 13, 43 | w3a 1088 |
. . 3
wff
(〈𝑔, 𝑠〉 ∈ CVecOLD
∧ 𝑛:ran 𝑔⟶ℝ ∧
∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦)))) |
45 | 44, 2, 4, 11 | coprab 7165 |
. 2
class
{〈〈𝑔,
𝑠〉, 𝑛〉 ∣ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))} |
46 | 1, 45 | wceq 1542 |
1
wff NrmCVec =
{〈〈𝑔, 𝑠〉, 𝑛〉 ∣ (〈𝑔, 𝑠〉 ∈ CVecOLD ∧ 𝑛:ran 𝑔⟶ℝ ∧ ∀𝑥 ∈ ran 𝑔(((𝑛‘𝑥) = 0 → 𝑥 = (GId‘𝑔)) ∧ ∀𝑦 ∈ ℂ (𝑛‘(𝑦𝑠𝑥)) = ((abs‘𝑦) · (𝑛‘𝑥)) ∧ ∀𝑦 ∈ ran 𝑔(𝑛‘(𝑥𝑔𝑦)) ≤ ((𝑛‘𝑥) + (𝑛‘𝑦))))} |