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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
isncvsngp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
isncvsngp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
isncvsngp.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isncvsngp.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion isncvsngp ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 isncvsngp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 isncvsngp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 isncvsngp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 isncvsngp.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5 isncvsngp.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
6 isnvc ⊢ ( 𝑊 ∈ NrmVec ↔ ( 𝑊 ∈ NrmMod ∧ 𝑊 ∈ LVec ) )
7 6 biancomi ⊢ ( 𝑊 ∈ NrmVec ↔ ( 𝑊 ∈ LVec ∧ 𝑊 ∈ NrmMod ) )
8 7 a1i ⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ NrmVec ↔ ( 𝑊 ∈ LVec ∧ 𝑊 ∈ NrmMod ) ) )
9 id ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂVec )
10 9 cvslvec ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ LVec )
11 10 biantrurd ⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ NrmMod ↔ ( 𝑊 ∈ LVec ∧ 𝑊 ∈ NrmMod ) ) )
12 9 cvsclm ⊢ ( 𝑊 ∈ ℂVec → 𝑊 ∈ ℂMod )
13 eqid ⊢ ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
14 1 2 3 4 5 13 isnlm ⊢ ( 𝑊 ∈ NrmMod ↔ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
15 3anass ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ↔ ( 𝑊 ∈ NrmGrp ∧ ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ) )
16 15 biancomi ⊢ ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ 𝑊 ∈ NrmGrp ) )
17 16 anbi1i ⊢ ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ 𝑊 ∈ NrmGrp ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
18 anass ⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ 𝑊 ∈ NrmGrp ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
19 17 18 bitri ⊢ ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
20 19 a1i ⊢ ( 𝑊 ∈ ℂMod → ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) ) )
21 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
22 4 5 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
23 cnnrg ⊢ ℂfld ∈ NrmRing
24 4 5 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
25 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
26 25 subrgnrg ⊢ ( ( ℂfld ∈ NrmRing ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) → ( ℂfld ↾s 𝐾 ) ∈ NrmRing )
27 23 24 26 sylancr ⊢ ( 𝑊 ∈ ℂMod → ( ℂfld ↾s 𝐾 ) ∈ NrmRing )
28 22 27 eqeltrd ⊢ ( 𝑊 ∈ ℂMod → 𝐹 ∈ NrmRing )
29 21 28 jca ⊢ ( 𝑊 ∈ ℂMod → ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) )
30 29 biantrurd ⊢ ( 𝑊 ∈ ℂMod → ( ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ( 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) ) )
31 ralcom ⊢ ( ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
32 22 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) ) )
33 subrgsubg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
34 eqid ⊢ ( norm ‘ ℂfld ) = ( norm ‘ ℂfld )
35 eqid ⊢ ( norm ‘ ( ℂfld ↾s 𝐾 ) ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) )
36 25 34 35 subgnm ⊢ ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) → ( norm ‘ ( ℂfld ↾s 𝐾 ) ) = ( ( norm ‘ ℂfld ) ↾ 𝐾 ) )
37 24 33 36 3syl ⊢ ( 𝑊 ∈ ℂMod → ( norm ‘ ( ℂfld ↾s 𝐾 ) ) = ( ( norm ‘ ℂfld ) ↾ 𝐾 ) )
38 32 37 eqtrd ⊢ ( 𝑊 ∈ ℂMod → ( norm ‘ 𝐹 ) = ( ( norm ‘ ℂfld ) ↾ 𝐾 ) )
39 38 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( norm ‘ 𝐹 ) = ( ( norm ‘ ℂfld ) ↾ 𝐾 ) )
40 39 fveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) = ( ( ( norm ‘ ℂfld ) ↾ 𝐾 ) ‘ 𝑘 ) )
41 cnfldnm ⊢ abs = ( norm ‘ ℂfld )
42 41 eqcomi ⊢ ( norm ‘ ℂfld ) = abs
43 42 reseq1i ⊢ ( ( norm ‘ ℂfld ) ↾ 𝐾 ) = ( abs ↾ 𝐾 )
44 43 fveq1i ⊢ ( ( ( norm ‘ ℂfld ) ↾ 𝐾 ) ‘ 𝑘 ) = ( ( abs ↾ 𝐾 ) ‘ 𝑘 )
45 fvres ⊢ ( 𝑘 ∈ 𝐾 → ( ( abs ↾ 𝐾 ) ‘ 𝑘 ) = ( abs ‘ 𝑘 ) )
46 45 ad2antll ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( abs ↾ 𝐾 ) ‘ 𝑘 ) = ( abs ‘ 𝑘 ) )
47 44 46 syl5eq ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( ( norm ‘ ℂfld ) ↾ 𝐾 ) ‘ 𝑘 ) = ( abs ‘ 𝑘 ) )
48 40 47 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) = ( abs ‘ 𝑘 ) )
49 48 oveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
50 49 eqeq2d ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾 ) ) → ( ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ↔ ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
51 50 2ralbidva ⊢ ( 𝑊 ∈ ℂMod → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
52 31 51 syl5bb ⊢ ( 𝑊 ∈ ℂMod → ( ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
53 52 anbi2d ⊢ ( 𝑊 ∈ ℂMod → ( ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
54 20 30 53 3bitr2d ⊢ ( 𝑊 ∈ ℂMod → ( ( ( 𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing ) ∧ ∀ 𝑘 ∈ 𝐾 ∀ 𝑥 ∈ 𝑉 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
55 14 54 syl5bb ⊢ ( 𝑊 ∈ ℂMod → ( 𝑊 ∈ NrmMod ↔ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
56 12 55 syl ⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ NrmMod ↔ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
57 8 11 56 3bitr2d ⊢ ( 𝑊 ∈ ℂVec → ( 𝑊 ∈ NrmVec ↔ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
58 57 pm5.32i ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmVec ) ↔ ( 𝑊 ∈ ℂVec ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
59 elin ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec ) )
60 59 biancomi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmVec ) )
61 3anass ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( 𝑊 ∈ ℂVec ∧ ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
62 58 60 61 3bitr4i ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )