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 ) )`