Step |
Hyp |
Ref |
Expression |
0 |
|
cnv |
⊢ NrmCVec |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
vs |
⊢ 𝑠 |
3 |
|
vn |
⊢ 𝑛 |
4 |
1
|
cv |
⊢ 𝑔 |
5 |
2
|
cv |
⊢ 𝑠 |
6 |
4 5
|
cop |
⊢ 〈 𝑔 , 𝑠 〉 |
7 |
|
cvc |
⊢ CVecOLD |
8 |
6 7
|
wcel |
⊢ 〈 𝑔 , 𝑠 〉 ∈ CVecOLD |
9 |
3
|
cv |
⊢ 𝑛 |
10 |
4
|
crn |
⊢ ran 𝑔 |
11 |
|
cr |
⊢ ℝ |
12 |
10 11 9
|
wf |
⊢ 𝑛 : ran 𝑔 ⟶ ℝ |
13 |
|
vx |
⊢ 𝑥 |
14 |
13
|
cv |
⊢ 𝑥 |
15 |
14 9
|
cfv |
⊢ ( 𝑛 ‘ 𝑥 ) |
16 |
|
cc0 |
⊢ 0 |
17 |
15 16
|
wceq |
⊢ ( 𝑛 ‘ 𝑥 ) = 0 |
18 |
|
cgi |
⊢ GId |
19 |
4 18
|
cfv |
⊢ ( GId ‘ 𝑔 ) |
20 |
14 19
|
wceq |
⊢ 𝑥 = ( GId ‘ 𝑔 ) |
21 |
17 20
|
wi |
⊢ ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) |
22 |
|
vy |
⊢ 𝑦 |
23 |
|
cc |
⊢ ℂ |
24 |
22
|
cv |
⊢ 𝑦 |
25 |
24 14 5
|
co |
⊢ ( 𝑦 𝑠 𝑥 ) |
26 |
25 9
|
cfv |
⊢ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) |
27 |
|
cabs |
⊢ abs |
28 |
24 27
|
cfv |
⊢ ( abs ‘ 𝑦 ) |
29 |
|
cmul |
⊢ · |
30 |
28 15 29
|
co |
⊢ ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) |
31 |
26 30
|
wceq |
⊢ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) |
32 |
31 22 23
|
wral |
⊢ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) |
33 |
14 24 4
|
co |
⊢ ( 𝑥 𝑔 𝑦 ) |
34 |
33 9
|
cfv |
⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) |
35 |
|
cle |
⊢ ≤ |
36 |
|
caddc |
⊢ + |
37 |
24 9
|
cfv |
⊢ ( 𝑛 ‘ 𝑦 ) |
38 |
15 37 36
|
co |
⊢ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) |
39 |
34 38 35
|
wbr |
⊢ ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) |
40 |
39 22 10
|
wral |
⊢ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) |
41 |
21 32 40
|
w3a |
⊢ ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) |
42 |
41 13 10
|
wral |
⊢ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) |
43 |
8 12 42
|
w3a |
⊢ ( 〈 𝑔 , 𝑠 〉 ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) |
44 |
43 1 2 3
|
coprab |
⊢ { 〈 〈 𝑔 , 𝑠 〉 , 𝑛 〉 ∣ ( 〈 𝑔 , 𝑠 〉 ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) } |
45 |
0 44
|
wceq |
⊢ NrmCVec = { 〈 〈 𝑔 , 𝑠 〉 , 𝑛 〉 ∣ ( 〈 𝑔 , 𝑠 〉 ∈ CVecOLD ∧ 𝑛 : ran 𝑔 ⟶ ℝ ∧ ∀ 𝑥 ∈ ran 𝑔 ( ( ( 𝑛 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑛 ‘ ( 𝑦 𝑠 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑛 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ran 𝑔 ( 𝑛 ‘ ( 𝑥 𝑔 𝑦 ) ) ≤ ( ( 𝑛 ‘ 𝑥 ) + ( 𝑛 ‘ 𝑦 ) ) ) ) } |