Step |
Hyp |
Ref |
Expression |
0 |
|
cnlm |
|- NrmMod |
1 |
|
vw |
|- w |
2 |
|
cngp |
|- NrmGrp |
3 |
|
clmod |
|- LMod |
4 |
2 3
|
cin |
|- ( NrmGrp i^i LMod ) |
5 |
|
csca |
|- Scalar |
6 |
1
|
cv |
|- w |
7 |
6 5
|
cfv |
|- ( Scalar ` w ) |
8 |
|
vf |
|- f |
9 |
8
|
cv |
|- f |
10 |
|
cnrg |
|- NrmRing |
11 |
9 10
|
wcel |
|- f e. NrmRing |
12 |
|
vx |
|- x |
13 |
|
cbs |
|- Base |
14 |
9 13
|
cfv |
|- ( Base ` f ) |
15 |
|
vy |
|- y |
16 |
6 13
|
cfv |
|- ( Base ` w ) |
17 |
|
cnm |
|- norm |
18 |
6 17
|
cfv |
|- ( norm ` w ) |
19 |
12
|
cv |
|- x |
20 |
|
cvsca |
|- .s |
21 |
6 20
|
cfv |
|- ( .s ` w ) |
22 |
15
|
cv |
|- y |
23 |
19 22 21
|
co |
|- ( x ( .s ` w ) y ) |
24 |
23 18
|
cfv |
|- ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) |
25 |
9 17
|
cfv |
|- ( norm ` f ) |
26 |
19 25
|
cfv |
|- ( ( norm ` f ) ` x ) |
27 |
|
cmul |
|- x. |
28 |
22 18
|
cfv |
|- ( ( norm ` w ) ` y ) |
29 |
26 28 27
|
co |
|- ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) |
30 |
24 29
|
wceq |
|- ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) |
31 |
30 15 16
|
wral |
|- A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) |
32 |
31 12 14
|
wral |
|- A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) |
33 |
11 32
|
wa |
|- ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) |
34 |
33 8 7
|
wsbc |
|- [. ( Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) |
35 |
34 1 4
|
crab |
|- { w e. ( NrmGrp i^i LMod ) | [. ( Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) } |
36 |
0 35
|
wceq |
|- NrmMod = { w e. ( NrmGrp i^i LMod ) | [. ( Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) } |