Step |
Hyp |
Ref |
Expression |
0 |
|
cnv |
|- NrmCVec |
1 |
|
vg |
|- g |
2 |
|
vs |
|- s |
3 |
|
vn |
|- n |
4 |
1
|
cv |
|- g |
5 |
2
|
cv |
|- s |
6 |
4 5
|
cop |
|- <. g , s >. |
7 |
|
cvc |
|- CVecOLD |
8 |
6 7
|
wcel |
|- <. g , s >. e. CVecOLD |
9 |
3
|
cv |
|- n |
10 |
4
|
crn |
|- ran g |
11 |
|
cr |
|- RR |
12 |
10 11 9
|
wf |
|- n : ran g --> RR |
13 |
|
vx |
|- x |
14 |
13
|
cv |
|- x |
15 |
14 9
|
cfv |
|- ( n ` x ) |
16 |
|
cc0 |
|- 0 |
17 |
15 16
|
wceq |
|- ( n ` x ) = 0 |
18 |
|
cgi |
|- GId |
19 |
4 18
|
cfv |
|- ( GId ` g ) |
20 |
14 19
|
wceq |
|- x = ( GId ` g ) |
21 |
17 20
|
wi |
|- ( ( n ` x ) = 0 -> x = ( GId ` g ) ) |
22 |
|
vy |
|- y |
23 |
|
cc |
|- CC |
24 |
22
|
cv |
|- y |
25 |
24 14 5
|
co |
|- ( y s x ) |
26 |
25 9
|
cfv |
|- ( n ` ( y s x ) ) |
27 |
|
cabs |
|- abs |
28 |
24 27
|
cfv |
|- ( abs ` y ) |
29 |
|
cmul |
|- x. |
30 |
28 15 29
|
co |
|- ( ( abs ` y ) x. ( n ` x ) ) |
31 |
26 30
|
wceq |
|- ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) |
32 |
31 22 23
|
wral |
|- A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) |
33 |
14 24 4
|
co |
|- ( x g y ) |
34 |
33 9
|
cfv |
|- ( n ` ( x g y ) ) |
35 |
|
cle |
|- <_ |
36 |
|
caddc |
|- + |
37 |
24 9
|
cfv |
|- ( n ` y ) |
38 |
15 37 36
|
co |
|- ( ( n ` x ) + ( n ` y ) ) |
39 |
34 38 35
|
wbr |
|- ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) |
40 |
39 22 10
|
wral |
|- A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) |
41 |
21 32 40
|
w3a |
|- ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) |
42 |
41 13 10
|
wral |
|- A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) |
43 |
8 12 42
|
w3a |
|- ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) |
44 |
43 1 2 3
|
coprab |
|- { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) } |
45 |
0 44
|
wceq |
|- NrmCVec = { <. <. g , s >. , n >. | ( <. g , s >. e. CVecOLD /\ n : ran g --> RR /\ A. x e. ran g ( ( ( n ` x ) = 0 -> x = ( GId ` g ) ) /\ A. y e. CC ( n ` ( y s x ) ) = ( ( abs ` y ) x. ( n ` x ) ) /\ A. y e. ran g ( n ` ( x g y ) ) <_ ( ( n ` x ) + ( n ` y ) ) ) ) } |