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	eqtr2id	⊢ ( ( 𝑈 ∈ 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 ≤ ( 𝑁 ‘ 𝐴 ) )