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 
|- A e. ~H
norm-ii.2 
|- B e. ~H
Assertion norm-ii-i 
|- ( normh ` ( A +h B ) ) <_ ( ( normh ` A ) + ( normh ` B ) )

Proof

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