Metamath Proof Explorer

Theorem ncvsi

Description: The properties of a normed subcomplex vector space, which is a vector space accompanied by a norm. (Contributed by NM, 11-Nov-2006) (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 )
ncvsi.m 
|- .- = ( -g ` W )
ncvsi.0 
|- .0. = ( 0g ` W )
Assertion ncvsi 
|- ( W e. ( NrmVec i^i CVec ) -> ( W e. CVec /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )

Proof

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 ncvsi.m 
 |-  .- = ( -g ` W )
7 ncvsi.0 
 |-  .0. = ( 0g ` W )
8 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 ) ) ) )
9 simp1 
 |-  ( ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> W e. CVec )
10 1 2 nmf 
 |-  ( W e. NrmGrp -> N : V --> RR )
11 10 3ad2ant2 
 |-  ( ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> N : V --> RR )
12 1 2 6 7 ngpi 
 |-  ( W e. NrmGrp -> ( W e. Grp /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) )
13 r19.26 
 |-  ( A. x e. V ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) <-> ( A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
14 simpll 
 |-  ( ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> ( ( N ` x ) = 0 <-> x = .0. ) )
15 simplr 
 |-  ( ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) )
16 simpr 
 |-  ( ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) )
17 14 15 16 3jca 
 |-  ( ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
18 17 ralimi 
 |-  ( A. x e. V ( ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
19 13 18 sylbir 
 |-  ( ( A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
20 19 ex 
 |-  ( A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) -> ( A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
21 20 3ad2ant3 
 |-  ( ( W e. Grp /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) ) ) -> ( A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
22 12 21 syl 
 |-  ( W e. NrmGrp -> ( A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
23 22 imp 
 |-  ( ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
24 23 3adant1 
 |-  ( ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
25 9 11 24 3jca 
 |-  ( ( W e. CVec /\ W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) -> ( W e. CVec /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
26 8 25 sylbi 
 |-  ( W e. ( NrmVec i^i CVec ) -> ( W e. CVec /\ N : V --> RR /\ A. x e. V ( ( ( N ` x ) = 0 <-> x = .0. ) /\ A. y e. V ( N ` ( x .- y ) ) <_ ( ( N ` x ) + ( N ` y ) ) /\ A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )