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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvge0.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvge0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 nvge0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvge0.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
3 2rp ⊢ 2 ∈ ℝ+
4 3 a1i ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 2 ∈ ℝ+ )
5 1 2 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℝ )
6 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
7 6 2 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
8 7 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 0vec ‘ 𝑈 ) ) = 0 )
9 1pneg1e0 ⊢ ( 1 + - 1 ) = 0
10 9 oveq1i ⊢ ( ( 1 + - 1 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = ( 0 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 )
11 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
12 1 11 6 nv0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 0 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = ( 0vec ‘ 𝑈 ) )
13 10 12 syl5req ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 0vec ‘ 𝑈 ) = ( ( 1 + - 1 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) )
14 neg1cn ⊢ - 1 ∈ ℂ
15 ax-1cn ⊢ 1 ∈ ℂ
16 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
17 1 16 11 nvdir ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + - 1 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
18 15 17 mp3anr1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 1 + - 1 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
19 14 18 mpanr1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 + - 1 ) ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
20 1 11 nvsid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) = 𝐴 )
21 20 oveq1d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
22 13 19 21 3eqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 0vec ‘ 𝑈 ) = ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) )
23 22 fveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 0vec ‘ 𝑈 ) ) = ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
24 8 23 eqtr3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 = ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
25 1 11 nvscl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
26 14 25 mp3an2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 )
27 1 16 2 nvtri ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
28 26 27 mpd3an3 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
29 24 28 eqbrtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) )
30 1 11 2 nvm1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) = ( 𝑁 ‘ 𝐴 ) )
31 30 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐴 ) ) )
32 5 recnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ ℂ )
33 32 2timesd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 2 · ( 𝑁 ‘ 𝐴 ) ) = ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ 𝐴 ) ) )
34 31 33 eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) + ( 𝑁 ‘ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) ) ) = ( 2 · ( 𝑁 ‘ 𝐴 ) ) )
35 29 34 breqtrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 2 · ( 𝑁 ‘ 𝐴 ) ) )
36 4 5 35 prodge0rd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑁 ‘ 𝐴 ) )