Metamath Proof Explorer

Theorem normlem7

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

Ref Expression
Hypotheses normlem1.1 ⊢ 𝑆 ∈ ℂ
normlem1.2 ⊢ 𝐹 ∈ ℋ
normlem1.3 ⊢ 𝐺 ∈ ℋ
normlem7.4 ⊢ ( abs ‘ 𝑆 ) = 1
Assertion normlem7 ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 ⊢ 𝑆 ∈ ℂ
2 normlem1.2 ⊢ 𝐹 ∈ ℋ
3 normlem1.3 ⊢ 𝐺 ∈ ℋ
4 normlem7.4 ⊢ ( abs ‘ 𝑆 ) = 1
5 eqid ⊢ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) = - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) )
6 1 2 3 5 normlem2 ⊢ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ
7 1 cjcli ⊢ ( ∗ ‘ 𝑆 ) ∈ ℂ
8 2 3 hicli ⊢ ( 𝐹 ·ih 𝐺 ) ∈ ℂ
9 7 8 mulcli ⊢ ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) ∈ ℂ
10 3 2 hicli ⊢ ( 𝐺 ·ih 𝐹 ) ∈ ℂ
11 1 10 mulcli ⊢ ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ∈ ℂ
12 9 11 addcli ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℂ
13 12 negrebi ⊢ ( - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ ↔ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ )
14 6 13 mpbi ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℝ
15 14 leabsi ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( abs ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
16 12 absnegi ⊢ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) = ( abs ‘ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
17 15 16 breqtrri ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) )
18 eqid ⊢ ( 𝐺 ·ih 𝐺 ) = ( 𝐺 ·ih 𝐺 )
19 eqid ⊢ ( 𝐹 ·ih 𝐹 ) = ( 𝐹 ·ih 𝐹 )
20 1 2 3 5 18 19 4 normlem6 ⊢ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) )
21 12 negcli ⊢ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ∈ ℂ
22 21 abscli ⊢ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) ∈ ℝ
23 2re ⊢ 2 ∈ ℝ
24 hiidge0 ⊢ ( 𝐺 ∈ ℋ → 0 ≤ ( 𝐺 ·ih 𝐺 ) )
25 hiidrcl ⊢ ( 𝐺 ∈ ℋ → ( 𝐺 ·ih 𝐺 ) ∈ ℝ )
26 3 25 ax-mp ⊢ ( 𝐺 ·ih 𝐺 ) ∈ ℝ
27 26 sqrtcli ⊢ ( 0 ≤ ( 𝐺 ·ih 𝐺 ) → ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) ∈ ℝ )
28 3 24 27 mp2b ⊢ ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) ∈ ℝ
29 hiidge0 ⊢ ( 𝐹 ∈ ℋ → 0 ≤ ( 𝐹 ·ih 𝐹 ) )
30 hiidrcl ⊢ ( 𝐹 ∈ ℋ → ( 𝐹 ·ih 𝐹 ) ∈ ℝ )
31 2 30 ax-mp ⊢ ( 𝐹 ·ih 𝐹 ) ∈ ℝ
32 31 sqrtcli ⊢ ( 0 ≤ ( 𝐹 ·ih 𝐹 ) → ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ∈ ℝ )
33 2 29 32 mp2b ⊢ ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ∈ ℝ
34 28 33 remulcli ⊢ ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) ∈ ℝ
35 23 34 remulcli ⊢ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) ) ∈ ℝ
36 14 22 35 letri ⊢ ( ( ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) ∧ ( abs ‘ - ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) ) ) → ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) ) )
37 17 20 36 mp2an ⊢ ( ( ( ∗ ‘ 𝑆 ) · ( 𝐹 ·ih 𝐺 ) ) + ( 𝑆 · ( 𝐺 ·ih 𝐹 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐺 ·ih 𝐺 ) ) · ( √ ‘ ( 𝐹 ·ih 𝐹 ) ) ) )