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=normCV⁡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=normCV⁡U
3 2rp ⊢2∈ℝ+
4 3 a1i ⊢U∈NrmCVec∧A∈X→2∈ℝ+
5 1 2 nvcl ⊢U∈NrmCVec∧A∈X→N⁡A∈ℝ
6 eqid ⊢0vec⁡U=0vec⁡U
7 6 2 nvz0 ⊢U∈NrmCVec→N⁡0vec⁡U=0
8 7 adantr ⊢U∈NrmCVec∧A∈X→N⁡0vec⁡U=0
9 1pneg1e0 ⊢1+-1=0
10 9 oveq1i ⊢1+-1⋅𝑠OLD⁡UA=0⋅𝑠OLD⁡UA
11 eqid ⊢⋅𝑠OLD⁡U=⋅𝑠OLD⁡U
12 1 11 6 nv0 ⊢U∈NrmCVec∧A∈X→0⋅𝑠OLD⁡UA=0vec⁡U
13 10 12 eqtr2id ⊢U∈NrmCVec∧A∈X→0vec⁡U=1+-1⋅𝑠OLD⁡UA
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⁡UA=1⋅𝑠OLD⁡UA+v⁡U-1⋅𝑠OLD⁡UA
18 15 17 mp3anr1 ⊢U∈NrmCVec∧−1∈ℂ∧A∈X→1+-1⋅𝑠OLD⁡UA=1⋅𝑠OLD⁡UA+v⁡U-1⋅𝑠OLD⁡UA
19 14 18 mpanr1 ⊢U∈NrmCVec∧A∈X→1+-1⋅𝑠OLD⁡UA=1⋅𝑠OLD⁡UA+v⁡U-1⋅𝑠OLD⁡UA
20 1 11 nvsid ⊢U∈NrmCVec∧A∈X→1⋅𝑠OLD⁡UA=A
21 20 oveq1d ⊢U∈NrmCVec∧A∈X→1⋅𝑠OLD⁡UA+v⁡U-1⋅𝑠OLD⁡UA=A+v⁡U-1⋅𝑠OLD⁡UA
22 13 19 21 3eqtrd ⊢U∈NrmCVec∧A∈X→0vec⁡U=A+v⁡U-1⋅𝑠OLD⁡UA
23 22 fveq2d ⊢U∈NrmCVec∧A∈X→N⁡0vec⁡U=N⁡A+v⁡U-1⋅𝑠OLD⁡UA
24 8 23 eqtr3d ⊢U∈NrmCVec∧A∈X→0=N⁡A+v⁡U-1⋅𝑠OLD⁡UA
25 1 11 nvscl ⊢U∈NrmCVec∧−1∈ℂ∧A∈X→-1⋅𝑠OLD⁡UA∈X
26 14 25 mp3an2 ⊢U∈NrmCVec∧A∈X→-1⋅𝑠OLD⁡UA∈X
27 1 16 2 nvtri ⊢U∈NrmCVec∧A∈X∧-1⋅𝑠OLD⁡UA∈X→N⁡A+v⁡U-1⋅𝑠OLD⁡UA≤N⁡A+N⁡-1⋅𝑠OLD⁡UA
28 26 27 mpd3an3 ⊢U∈NrmCVec∧A∈X→N⁡A+v⁡U-1⋅𝑠OLD⁡UA≤N⁡A+N⁡-1⋅𝑠OLD⁡UA
29 24 28 eqbrtrd ⊢U∈NrmCVec∧A∈X→0≤N⁡A+N⁡-1⋅𝑠OLD⁡UA
30 1 11 2 nvm1 ⊢U∈NrmCVec∧A∈X→N⁡-1⋅𝑠OLD⁡UA=N⁡A
31 30 oveq2d ⊢U∈NrmCVec∧A∈X→N⁡A+N⁡-1⋅𝑠OLD⁡UA=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⁡UA=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