Theorem normlem5

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 10-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	normlem1.1	⊢ 𝑆 ∈ ℂ
	normlem1.2	⊢ 𝐹 ∈ ℋ
	normlem1.3	⊢ 𝐺 ∈ ℋ
	normlem2.4	⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
	normlem3.5	⊢ 𝐴 = ( 𝐺 ·ih 𝐺 )
	normlem3.6	⊢ 𝐶 = ( 𝐹 ·ih 𝐹 )
	normlem4.7	⊢ 𝑅 ∈ ℝ
	normlem4.8	⊢ ( abs ‘ 𝑆 ) = 1
Assertion	normlem5	⊢ 0 ≤ ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		normlem1.1	⊢ 𝑆 ∈ ℂ
2		normlem1.2	⊢ 𝐹 ∈ ℋ
3		normlem1.3	⊢ 𝐺 ∈ ℋ
4		normlem2.4	⊢ 𝐵 = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
5		normlem3.5	⊢ 𝐴 = ( 𝐺 ·ih 𝐺 )
6		normlem3.6	⊢ 𝐶 = ( 𝐹 ·ih 𝐹 )
7		normlem4.7	⊢ 𝑅 ∈ ℝ
8		normlem4.8	⊢ ( abs ‘ 𝑆 ) = 1
9	7	recni	⊢ 𝑅 ∈ ℂ
10	1 9	mulcli	⊢ ( 𝑆 · 𝑅 ) ∈ ℂ
11	10 3	hvmulcli	⊢ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ∈ ℋ
12	2 11	hvsubcli	⊢ ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ∈ ℋ
13		hiidge0	⊢ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ∈ ℋ → 0 ≤ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ) )
14	12 13	ax-mp	⊢ 0 ≤ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) )
15	1 2 3 4 5 6 7 8	normlem4	⊢ ( ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ·ih ( 𝐹 −ℎ ( ( 𝑆 · 𝑅 ) ·ℎ 𝐺 ) ) ) = ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )
16	14 15	breqtri	⊢ 0 ≤ ( ( ( 𝐴 · ( 𝑅 ↑ 2 ) ) + ( 𝐵 · 𝑅 ) ) + 𝐶 )