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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
isncvsngp.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
isncvsngp.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
isncvsngp.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isncvsngp.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
ncvsi.m ⊢ − = ( -g ‘ 𝑊 )
ncvsi.0 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion ncvsi ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → ( 𝑊 ∈ ℂVec ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( 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 ncvsi.m ⊢ − = ( -g ‘ 𝑊 )
7 ncvsi.0 ⊢ 0 = ( 0g ‘ 𝑊 )
8 1 2 3 4 5 isncvsngp ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) ↔ ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
9 simp1 ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → 𝑊 ∈ ℂVec )
10 1 2 nmf ⊢ ( 𝑊 ∈ NrmGrp → 𝑁 : 𝑉 ⟶ ℝ )
11 10 3ad2ant2 ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → 𝑁 : 𝑉 ⟶ ℝ )
12 1 2 6 7 ngpi ⊢ ( 𝑊 ∈ NrmGrp → ( 𝑊 ∈ Grp ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
13 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
14 simpll ⊢ ( ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
15 simplr ⊢ ( ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
16 simpr ⊢ ( ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) )
17 14 15 16 3jca ⊢ ( ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
18 17 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
19 13 18 sylbir ⊢ ( ( ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
20 19 ex ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
21 20 3ad2ant3 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
22 12 21 syl ⊢ ( 𝑊 ∈ NrmGrp → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
23 22 imp ⊢ ( ( 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
24 23 3adant1 ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) )
25 9 11 24 3jca ⊢ ( ( 𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) → ( 𝑊 ∈ ℂVec ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )
26 8 25 sylbi ⊢ ( 𝑊 ∈ ( NrmVec ∩ ℂVec ) → ( 𝑊 ∈ ℂVec ∧ 𝑁 : 𝑉 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑉 ( ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( 𝑁 ‘ ( 𝑥 − 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ∧ ∀ 𝑘 ∈ 𝐾 ( 𝑁 ‘ ( 𝑘 · 𝑥 ) ) = ( ( abs ‘ 𝑘 ) · ( 𝑁 ‘ 𝑥 ) ) ) ) )