Metamath Proof Explorer

Theorem isncvsngp

Description: A normed subcomplex vector space is a subcomplex vector space which is a normed group with a positively homogeneous norm. (Contributed by NM, 5-Jun-2008) (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 )
Assertion 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 ) ) ) )

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 isnvc 
 |-  ( W e. NrmVec <-> ( W e. NrmMod /\ W e. LVec ) )
7 6 biancomi 
 |-  ( W e. NrmVec <-> ( W e. LVec /\ W e. NrmMod ) )
8 7 a1i 
 |-  ( W e. CVec -> ( W e. NrmVec <-> ( W e. LVec /\ W e. NrmMod ) ) )
9 id 
 |-  ( W e. CVec -> W e. CVec )
10 9 cvslvec 
 |-  ( W e. CVec -> W e. LVec )
11 10 biantrurd 
 |-  ( W e. CVec -> ( W e. NrmMod <-> ( W e. LVec /\ W e. NrmMod ) ) )
12 9 cvsclm 
 |-  ( W e. CVec -> W e. CMod )
13 eqid 
 |-  ( norm ` F ) = ( norm ` F )
14 1 2 3 4 5 13 isnlm 
 |-  ( W e. NrmMod <-> ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) )
15 3anass 
 |-  ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) <-> ( W e. NrmGrp /\ ( W e. LMod /\ F e. NrmRing ) ) )
16 15 biancomi 
 |-  ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) <-> ( ( W e. LMod /\ F e. NrmRing ) /\ W e. NrmGrp ) )
17 16 anbi1i 
 |-  ( ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( ( ( W e. LMod /\ F e. NrmRing ) /\ W e. NrmGrp ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) )
18 anass 
 |-  ( ( ( ( W e. LMod /\ F e. NrmRing ) /\ W e. NrmGrp ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( ( W e. LMod /\ F e. NrmRing ) /\ ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) ) )
19 17 18 bitri 
 |-  ( ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( ( W e. LMod /\ F e. NrmRing ) /\ ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) ) )
20 19 a1i 
 |-  ( W e. CMod -> ( ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( ( W e. LMod /\ F e. NrmRing ) /\ ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) ) ) )
21 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
22 4 5 clmsca 
 |-  ( W e. CMod -> F = ( CCfld |`s K ) )
23 cnnrg 
 |-  CCfld e. NrmRing
24 4 5 clmsubrg 
 |-  ( W e. CMod -> K e. ( SubRing ` CCfld ) )
25 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
26 25 subrgnrg 
 |-  ( ( CCfld e. NrmRing /\ K e. ( SubRing ` CCfld ) ) -> ( CCfld |`s K ) e. NrmRing )
27 23 24 26 sylancr 
 |-  ( W e. CMod -> ( CCfld |`s K ) e. NrmRing )
28 22 27 eqeltrd 
 |-  ( W e. CMod -> F e. NrmRing )
29 21 28 jca 
 |-  ( W e. CMod -> ( W e. LMod /\ F e. NrmRing ) )
30 29 biantrurd 
 |-  ( W e. CMod -> ( ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( ( W e. LMod /\ F e. NrmRing ) /\ ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) ) ) )
31 ralcom 
 |-  ( A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) <-> A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) )
32 22 fveq2d 
 |-  ( W e. CMod -> ( norm ` F ) = ( norm ` ( CCfld |`s K ) ) )
33 subrgsubg 
 |-  ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
34 eqid 
 |-  ( norm ` CCfld ) = ( norm ` CCfld )
35 eqid 
 |-  ( norm ` ( CCfld |`s K ) ) = ( norm ` ( CCfld |`s K ) )
36 25 34 35 subgnm 
 |-  ( K e. ( SubGrp ` CCfld ) -> ( norm ` ( CCfld |`s K ) ) = ( ( norm ` CCfld ) |` K ) )
37 24 33 36 3syl 
 |-  ( W e. CMod -> ( norm ` ( CCfld |`s K ) ) = ( ( norm ` CCfld ) |` K ) )
38 32 37 eqtrd 
 |-  ( W e. CMod -> ( norm ` F ) = ( ( norm ` CCfld ) |` K ) )
39 38 adantr 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( norm ` F ) = ( ( norm ` CCfld ) |` K ) )
40 39 fveq1d 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( norm ` F ) ` k ) = ( ( ( norm ` CCfld ) |` K ) ` k ) )
41 cnfldnm 
 |-  abs = ( norm ` CCfld )
42 41 eqcomi 
 |-  ( norm ` CCfld ) = abs
43 42 reseq1i 
 |-  ( ( norm ` CCfld ) |` K ) = ( abs |` K )
44 43 fveq1i 
 |-  ( ( ( norm ` CCfld ) |` K ) ` k ) = ( ( abs |` K ) ` k )
45 fvres 
 |-  ( k e. K -> ( ( abs |` K ) ` k ) = ( abs ` k ) )
46 45 ad2antll 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( abs |` K ) ` k ) = ( abs ` k ) )
47 44 46 syl5eq 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( ( norm ` CCfld ) |` K ) ` k ) = ( abs ` k ) )
48 40 47 eqtrd 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( norm ` F ) ` k ) = ( abs ` k ) )
49 48 oveq1d 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) = ( ( abs ` k ) x. ( N ` x ) ) )
50 49 eqeq2d 
 |-  ( ( W e. CMod /\ ( x e. V /\ k e. K ) ) -> ( ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) <-> ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
51 50 2ralbidva 
 |-  ( W e. CMod -> ( A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) <-> A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
52 31 51 syl5bb 
 |-  ( W e. CMod -> ( A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) <-> A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) )
53 52 anbi2d 
 |-  ( W e. CMod -> ( ( W e. NrmGrp /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
54 20 30 53 3bitr2d 
 |-  ( W e. CMod -> ( ( ( W e. NrmGrp /\ W e. LMod /\ F e. NrmRing ) /\ A. k e. K A. x e. V ( N ` ( k .x. x ) ) = ( ( ( norm ` F ) ` k ) x. ( N ` x ) ) ) <-> ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
55 14 54 syl5bb 
 |-  ( W e. CMod -> ( W e. NrmMod <-> ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
56 12 55 syl 
 |-  ( W e. CVec -> ( W e. NrmMod <-> ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
57 8 11 56 3bitr2d 
 |-  ( W e. CVec -> ( W e. NrmVec <-> ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
58 57 pm5.32i 
 |-  ( ( W e. CVec /\ W e. NrmVec ) <-> ( W e. CVec /\ ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
59 elin 
 |-  ( W e. ( NrmVec i^i CVec ) <-> ( W e. NrmVec /\ W e. CVec ) )
60 59 biancomi 
 |-  ( W e. ( NrmVec i^i CVec ) <-> ( W e. CVec /\ W e. NrmVec ) )
61 3anass 
 |-  ( ( 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 /\ ( W e. NrmGrp /\ A. x e. V A. k e. K ( N ` ( k .x. x ) ) = ( ( abs ` k ) x. ( N ` x ) ) ) ) )
62 58 60 61 3bitr4i 
 |-  ( 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 ) ) ) )