Metamath Proof Explorer

Theorem norm-ii-i

Description: Triangle inequality for norms. Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses norm-ii.1 ⊢ 𝐴 ∈ ℋ
norm-ii.2 ⊢ 𝐵 ∈ ℋ
Assertion norm-ii-i ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) + ( normℎ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 norm-ii.1 ⊢ 𝐴 ∈ ℋ
2 norm-ii.2 ⊢ 𝐵 ∈ ℋ
3 1re ⊢ 1 ∈ ℝ
4 ax-1cn ⊢ 1 ∈ ℂ
5 4 cjrebi ⊢ ( 1 ∈ ℝ ↔ ( ∗ ‘ 1 ) = 1 )
6 3 5 mpbi ⊢ ( ∗ ‘ 1 ) = 1
7 6 oveq1i ⊢ ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) = ( 1 · ( 𝐵 ·ih 𝐴 ) )
8 2 1 hicli ⊢ ( 𝐵 ·ih 𝐴 ) ∈ ℂ
9 8 mulid2i ⊢ ( 1 · ( 𝐵 ·ih 𝐴 ) ) = ( 𝐵 ·ih 𝐴 )
10 7 9 eqtri ⊢ ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) = ( 𝐵 ·ih 𝐴 )
11 1 2 hicli ⊢ ( 𝐴 ·ih 𝐵 ) ∈ ℂ
12 11 mulid2i ⊢ ( 1 · ( 𝐴 ·ih 𝐵 ) ) = ( 𝐴 ·ih 𝐵 )
13 10 12 oveq12i ⊢ ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) = ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) )
14 abs1 ⊢ ( abs ‘ 1 ) = 1
15 4 2 1 14 normlem7 ⊢ ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) )
16 13 15 eqbrtrri ⊢ ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) )
17 eqid ⊢ - ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) = - ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) )
18 4 2 1 17 normlem2 ⊢ - ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ
19 4 cjcli ⊢ ( ∗ ‘ 1 ) ∈ ℂ
20 19 8 mulcli ⊢ ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) ∈ ℂ
21 4 11 mulcli ⊢ ( 1 · ( 𝐴 ·ih 𝐵 ) ) ∈ ℂ
22 20 21 addcli ⊢ ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℂ
23 22 negrebi ⊢ ( - ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ ↔ ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ )
24 18 23 mpbi ⊢ ( ( ( ∗ ‘ 1 ) · ( 𝐵 ·ih 𝐴 ) ) + ( 1 · ( 𝐴 ·ih 𝐵 ) ) ) ∈ ℝ
25 13 24 eqeltrri ⊢ ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) ∈ ℝ
26 2re ⊢ 2 ∈ ℝ
27 hiidge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( 𝐴 ·ih 𝐴 ) )
28 1 27 ax-mp ⊢ 0 ≤ ( 𝐴 ·ih 𝐴 )
29 hiidrcl ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ·ih 𝐴 ) ∈ ℝ )
30 1 29 ax-mp ⊢ ( 𝐴 ·ih 𝐴 ) ∈ ℝ
31 30 sqrtcli ⊢ ( 0 ≤ ( 𝐴 ·ih 𝐴 ) → ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ )
32 28 31 ax-mp ⊢ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℝ
33 hiidge0 ⊢ ( 𝐵 ∈ ℋ → 0 ≤ ( 𝐵 ·ih 𝐵 ) )
34 2 33 ax-mp ⊢ 0 ≤ ( 𝐵 ·ih 𝐵 )
35 hiidrcl ⊢ ( 𝐵 ∈ ℋ → ( 𝐵 ·ih 𝐵 ) ∈ ℝ )
36 2 35 ax-mp ⊢ ( 𝐵 ·ih 𝐵 ) ∈ ℝ
37 36 sqrtcli ⊢ ( 0 ≤ ( 𝐵 ·ih 𝐵 ) → ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ∈ ℝ )
38 34 37 ax-mp ⊢ ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ∈ ℝ
39 32 38 remulcli ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ∈ ℝ
40 26 39 remulcli ⊢ ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ∈ ℝ
41 30 36 readdcli ⊢ ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) ∈ ℝ
42 25 40 41 leadd2i ⊢ ( ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) ≤ ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ↔ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ) )
43 16 42 mpbi ⊢ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) ) ≤ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) )
44 1 2 1 2 normlem8 ⊢ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) )
45 11 8 addcomi ⊢ ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) = ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) )
46 45 oveq2i ⊢ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) )
47 44 46 eqtri ⊢ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐵 ·ih 𝐴 ) + ( 𝐴 ·ih 𝐵 ) ) )
48 32 recni ⊢ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∈ ℂ
49 38 recni ⊢ ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ∈ ℂ
50 48 49 binom2i ⊢ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) = ( ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) )
51 48 sqcli ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) ∈ ℂ
52 2cn ⊢ 2 ∈ ℂ
53 48 49 mulcli ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ∈ ℂ
54 52 53 mulcli ⊢ ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ∈ ℂ
55 49 sqcli ⊢ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) ∈ ℂ
56 51 54 55 add32i ⊢ ( ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ) + ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) + ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) )
57 30 sqsqrti ⊢ ( 0 ≤ ( 𝐴 ·ih 𝐴 ) → ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 ) )
58 28 57 ax-mp ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 )
59 36 sqsqrti ⊢ ( 0 ≤ ( 𝐵 ·ih 𝐵 ) → ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) = ( 𝐵 ·ih 𝐵 ) )
60 34 59 ax-mp ⊢ ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) = ( 𝐵 ·ih 𝐵 )
61 58 60 oveq12i ⊢ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) + ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) ) = ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) )
62 61 oveq1i ⊢ ( ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ↑ 2 ) + ( ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ↑ 2 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) )
63 50 56 62 3eqtri ⊢ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( 2 · ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) · ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ) )
64 43 47 63 3brtr4i ⊢ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 )
65 1 2 hvaddcli ⊢ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ
66 hiidge0 ⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → 0 ≤ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) )
67 65 66 ax-mp ⊢ 0 ≤ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) )
68 32 38 readdcli ⊢ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ∈ ℝ
69 68 sqge0i ⊢ 0 ≤ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 )
70 hiidrcl ⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ∈ ℝ )
71 65 70 ax-mp ⊢ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ∈ ℝ
72 68 resqcli ⊢ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ∈ ℝ
73 71 72 sqrtlei ⊢ ( ( 0 ≤ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ∧ 0 ≤ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ) → ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ↔ ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ) ≤ ( √ ‘ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ) ) )
74 67 69 73 mp2an ⊢ ( ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ↔ ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ) ≤ ( √ ‘ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ) )
75 64 74 mpbi ⊢ ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ) ≤ ( √ ‘ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) )
76 30 sqrtge0i ⊢ ( 0 ≤ ( 𝐴 ·ih 𝐴 ) → 0 ≤ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
77 28 76 ax-mp ⊢ 0 ≤ ( √ ‘ ( 𝐴 ·ih 𝐴 ) )
78 36 sqrtge0i ⊢ ( 0 ≤ ( 𝐵 ·ih 𝐵 ) → 0 ≤ ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
79 34 78 ax-mp ⊢ 0 ≤ ( √ ‘ ( 𝐵 ·ih 𝐵 ) )
80 32 38 addge0i ⊢ ( ( 0 ≤ ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) ∧ 0 ≤ ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) → 0 ≤ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) )
81 77 79 80 mp2an ⊢ 0 ≤ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
82 68 sqrtsqi ⊢ ( 0 ≤ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) → ( √ ‘ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ) = ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) )
83 81 82 ax-mp ⊢ ( √ ‘ ( ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) ) ↑ 2 ) ) = ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
84 75 83 breqtri ⊢ ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ) ≤ ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
85 normval ⊢ ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ → ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) ) )
86 65 85 ax-mp ⊢ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( √ ‘ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) )
87 normval ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) )
88 1 87 ax-mp ⊢ ( normℎ ‘ 𝐴 ) = ( √ ‘ ( 𝐴 ·ih 𝐴 ) )
89 normval ⊢ ( 𝐵 ∈ ℋ → ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
90 2 89 ax-mp ⊢ ( normℎ ‘ 𝐵 ) = ( √ ‘ ( 𝐵 ·ih 𝐵 ) )
91 88 90 oveq12i ⊢ ( ( normℎ ‘ 𝐴 ) + ( normℎ ‘ 𝐵 ) ) = ( ( √ ‘ ( 𝐴 ·ih 𝐴 ) ) + ( √ ‘ ( 𝐵 ·ih 𝐵 ) ) )
92 84 86 91 3brtr4i ⊢ ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ≤ ( ( normℎ ‘ 𝐴 ) + ( normℎ ‘ 𝐵 ) )