Metamath Proof Explorer

Theorem nvge0

Description: The norm of a normed complex vector space is nonnegative. Second part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 28-Nov-2006) (Proof shortened by AV, 10-Jul-2022) (New usage is discouraged.)

Ref Expression
Hypotheses nvge0.1 ⊢ X = BaseSet ⁡ U
nvge0.6 ⊢ N = norm CV ⁡ U
Assertion nvge0 ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ≤ N ⁡ A

Proof

Step Hyp Ref Expression
1 nvge0.1 ⊢ X = BaseSet ⁡ U
2 nvge0.6 ⊢ N = norm CV ⁡ U
3 2rp ⊢ 2 ∈ ℝ +
4 3 a1i ⊢ U ∈ NrmCVec ∧ A ∈ X → 2 ∈ ℝ +
5 1 2 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℝ
6 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
7 6 2 nvz0 ⊢ U ∈ NrmCVec → N ⁡ 0 vec ⁡ U = 0
8 7 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 0 vec ⁡ U = 0
9 1pneg1e0 ⊢ 1 + -1 = 0
10 9 oveq1i ⊢ 1 + -1 ⋅ 𝑠OLD ⁡ U A = 0 ⋅ 𝑠OLD ⁡ U A
11 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
12 1 11 6 nv0 ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ⋅ 𝑠OLD ⁡ U A = 0 vec ⁡ U
13 10 12 eqtr2id ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 vec ⁡ U = 1 + -1 ⋅ 𝑠OLD ⁡ U A
14 neg1cn ⊢ − 1 ∈ ℂ
15 ax-1cn ⊢ 1 ∈ ℂ
16 eqid ⊢ + v ⁡ U = + v ⁡ U
17 1 16 11 nvdir ⊢ U ∈ NrmCVec ∧ 1 ∈ ℂ ∧ − 1 ∈ ℂ ∧ A ∈ X → 1 + -1 ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
18 15 17 mp3anr1 ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → 1 + -1 ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
19 14 18 mpanr1 ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 + -1 ⋅ 𝑠OLD ⁡ U A = 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
20 1 11 nvsid ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A = A
21 20 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → 1 ⋅ 𝑠OLD ⁡ U A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
22 13 19 21 3eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 vec ⁡ U = A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
23 22 fveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ 0 vec ⁡ U = N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
24 8 23 eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 = N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A
25 1 11 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → -1 ⋅ 𝑠OLD ⁡ U A ∈ X
26 14 25 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 ⋅ 𝑠OLD ⁡ U A ∈ X
27 1 16 2 nvtri ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U A ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A ≤ N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U A
28 26 27 mpd3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U A ≤ N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U A
29 24 28 eqbrtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ≤ N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U A
30 1 11 2 nvm1 ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ -1 ⋅ 𝑠OLD ⁡ U A = N ⁡ A
31 30 oveq2d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U A = N ⁡ A + N ⁡ A
32 5 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A ∈ ℂ
33 32 2timesd ⊢ U ∈ NrmCVec ∧ A ∈ X → 2 ⁢ N ⁡ A = N ⁡ A + N ⁡ A
34 31 33 eqtr4d ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A + N ⁡ -1 ⋅ 𝑠OLD ⁡ U A = 2 ⁢ N ⁡ A
35 29 34 breqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ≤ 2 ⁢ N ⁡ A
36 4 5 35 prodge0rd ⊢ U ∈ NrmCVec ∧ A ∈ X → 0 ≤ N ⁡ A