Description: Properties that determine a normed subcomplex vector space. (Contributed by NM, 15-Apr-2007) (Revised by AV, 7-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | isncvsngp.v | |- V = ( Base ` W ) |
|
| isncvsngp.n | |- N = ( norm ` W ) |
||
| isncvsngp.s | |- .x. = ( .s ` W ) |
||
| isncvsngp.f | |- F = ( Scalar ` W ) |
||
| isncvsngp.k | |- K = ( Base ` F ) |
||
| isncvsngpd.v | |- ( ph -> W e. CVec ) |
||
| isncvsngpd.g | |- ( ph -> W e. NrmGrp ) |
||
| isncvsngpd.t | |- ( ( ph /\ ( x e. V /\ k e. K ) ) -> ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) |
||
| Assertion | isncvsngpd | |- ( ph -> W e. ( NrmVec i^i CVec ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isncvsngp.v | |- V = ( Base ` W ) |
|
| 2 | isncvsngp.n | |- N = ( norm ` W ) |
|
| 3 | isncvsngp.s | |- .x. = ( .s ` W ) |
|
| 4 | isncvsngp.f | |- F = ( Scalar ` W ) |
|
| 5 | isncvsngp.k | |- K = ( Base ` F ) |
|
| 6 | isncvsngpd.v | |- ( ph -> W e. CVec ) |
|
| 7 | isncvsngpd.g | |- ( ph -> W e. NrmGrp ) |
|
| 8 | isncvsngpd.t | |- ( ( ph /\ ( x e. V /\ k e. K ) ) -> ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) |
|
| 9 | 8 | ralrimivva | |- ( ph -> A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) |
| 10 | 1 2 3 4 5 | isncvsngp | |- ( W e. ( NrmVec i^i CVec ) <-> ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) |
| 11 | 6 7 9 10 | syl3anbrc | |- ( ph -> W e. ( NrmVec i^i CVec ) ) |