Metamath Proof Explorer

Theorem tcphcphlem1

Description: Lemma for tcphcph : the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n 
|- G = ( toCPreHil ` W )
tcphcph.v 
|- V = ( Base ` W )
tcphcph.f 
|- F = ( Scalar ` W )
tcphcph.1 
|- ( ph -> W e. PreHil )
tcphcph.2 
|- ( ph -> F = ( CCfld |`s K ) )
tcphcph.h 
|- ., = ( .i ` W )
tcphcph.3 
|- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
tcphcph.4 
|- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
tcphcph.k 
|- K = ( Base ` F )
tcphcph.m 
|- .- = ( -g ` W )
tcphcphlem1.3 
|- ( ph -> X e. V )
tcphcphlem1.4 
|- ( ph -> Y e. V )
Assertion tcphcphlem1 
|- ( ph -> ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) <_ ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphcph.v 
 |-  V = ( Base ` W )
3 tcphcph.f 
 |-  F = ( Scalar ` W )
4 tcphcph.1 
 |-  ( ph -> W e. PreHil )
5 tcphcph.2 
 |-  ( ph -> F = ( CCfld |`s K ) )
6 tcphcph.h 
 |-  ., = ( .i ` W )
7 tcphcph.3 
 |-  ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqrt ` x ) e. K )
8 tcphcph.4 
 |-  ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )
9 tcphcph.k 
 |-  K = ( Base ` F )
10 tcphcph.m 
 |-  .- = ( -g ` W )
11 tcphcphlem1.3 
 |-  ( ph -> X e. V )
12 tcphcphlem1.4 
 |-  ( ph -> Y e. V )
13 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
14 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
15 4 13 14 3syl 
 |-  ( ph -> W e. Grp )
16 2 10 grpsubcl 
 |-  ( ( W e. Grp /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V )
17 15 11 12 16 syl3anc 
 |-  ( ph -> ( X .- Y ) e. V )
18 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ ( X .- Y ) e. V ) -> ( ( X .- Y ) ., ( X .- Y ) ) e. RR )
19 17 18 mpdan 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) e. RR )
20 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )
21 11 20 mpdan 
 |-  ( ph -> ( X ., X ) e. RR )
22 1 2 3 4 5 6 tcphcphlem3 
 |-  ( ( ph /\ Y e. V ) -> ( Y ., Y ) e. RR )
23 12 22 mpdan 
 |-  ( ph -> ( Y ., Y ) e. RR )
24 21 23 readdcld 
 |-  ( ph -> ( ( X ., X ) + ( Y ., Y ) ) e. RR )
25 1 2 3 4 5 phclm 
 |-  ( ph -> W e. CMod )
26 3 9 clmsscn 
 |-  ( W e. CMod -> K C_ CC )
27 25 26 syl 
 |-  ( ph -> K C_ CC )
28 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( X ., Y ) e. K )
29 4 11 12 28 syl3anc 
 |-  ( ph -> ( X ., Y ) e. K )
30 27 29 sseldd 
 |-  ( ph -> ( X ., Y ) e. CC )
31 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ Y e. V /\ X e. V ) -> ( Y ., X ) e. K )
32 4 12 11 31 syl3anc 
 |-  ( ph -> ( Y ., X ) e. K )
33 27 32 sseldd 
 |-  ( ph -> ( Y ., X ) e. CC )
34 30 33 addcld 
 |-  ( ph -> ( ( X ., Y ) + ( Y ., X ) ) e. CC )
35 34 abscld 
 |-  ( ph -> ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) e. RR )
36 24 35 readdcld 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) e. RR )
37 21 recnd 
 |-  ( ph -> ( X ., X ) e. CC )
38 2re 
 |-  2 e. RR
39 oveq12 
 |-  ( ( x = X /\ x = X ) -> ( x ., x ) = ( X ., X ) )
40 39 anidms 
 |-  ( x = X -> ( x ., x ) = ( X ., X ) )
41 40 breq2d 
 |-  ( x = X -> ( 0 <_ ( x ., x ) <-> 0 <_ ( X ., X ) ) )
42 8 ralrimiva 
 |-  ( ph -> A. x e. V 0 <_ ( x ., x ) )
43 41 42 11 rspcdva 
 |-  ( ph -> 0 <_ ( X ., X ) )
44 21 43 resqrtcld 
 |-  ( ph -> ( sqrt ` ( X ., X ) ) e. RR )
45 oveq12 
 |-  ( ( x = Y /\ x = Y ) -> ( x ., x ) = ( Y ., Y ) )
46 45 anidms 
 |-  ( x = Y -> ( x ., x ) = ( Y ., Y ) )
47 46 breq2d 
 |-  ( x = Y -> ( 0 <_ ( x ., x ) <-> 0 <_ ( Y ., Y ) ) )
48 47 42 12 rspcdva 
 |-  ( ph -> 0 <_ ( Y ., Y ) )
49 23 48 resqrtcld 
 |-  ( ph -> ( sqrt ` ( Y ., Y ) ) e. RR )
50 44 49 remulcld 
 |-  ( ph -> ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) e. RR )
51 remulcl 
 |-  ( ( 2 e. RR /\ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) e. RR ) -> ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) e. RR )
52 38 50 51 sylancr 
 |-  ( ph -> ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) e. RR )
53 52 recnd 
 |-  ( ph -> ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) e. CC )
54 23 recnd 
 |-  ( ph -> ( Y ., Y ) e. CC )
55 37 53 54 add32d 
 |-  ( ph -> ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) = ( ( ( X ., X ) + ( Y ., Y ) ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) )
56 24 52 readdcld 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) e. RR )
57 55 56 eqeltrd 
 |-  ( ph -> ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) e. RR )
58 oveq12 
 |-  ( ( x = ( X .- Y ) /\ x = ( X .- Y ) ) -> ( x ., x ) = ( ( X .- Y ) ., ( X .- Y ) ) )
59 58 anidms 
 |-  ( x = ( X .- Y ) -> ( x ., x ) = ( ( X .- Y ) ., ( X .- Y ) ) )
60 59 breq2d 
 |-  ( x = ( X .- Y ) -> ( 0 <_ ( x ., x ) <-> 0 <_ ( ( X .- Y ) ., ( X .- Y ) ) ) )
61 60 42 17 rspcdva 
 |-  ( ph -> 0 <_ ( ( X .- Y ) ., ( X .- Y ) ) )
62 19 61 absidd 
 |-  ( ph -> ( abs ` ( ( X .- Y ) ., ( X .- Y ) ) ) = ( ( X .- Y ) ., ( X .- Y ) ) )
63 3 clmadd 
 |-  ( W e. CMod -> + = ( +g ` F ) )
64 25 63 syl 
 |-  ( ph -> + = ( +g ` F ) )
65 64 oveqd 
 |-  ( ph -> ( ( X ., X ) + ( Y ., Y ) ) = ( ( X ., X ) ( +g ` F ) ( Y ., Y ) ) )
66 64 oveqd 
 |-  ( ph -> ( ( X ., Y ) + ( Y ., X ) ) = ( ( X ., Y ) ( +g ` F ) ( Y ., X ) ) )
67 65 66 oveq12d 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) ( -g ` F ) ( ( X ., Y ) + ( Y ., X ) ) ) = ( ( ( X ., X ) ( +g ` F ) ( Y ., Y ) ) ( -g ` F ) ( ( X ., Y ) ( +g ` F ) ( Y ., X ) ) ) )
68 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ X e. V /\ X e. V ) -> ( X ., X ) e. K )
69 4 11 11 68 syl3anc 
 |-  ( ph -> ( X ., X ) e. K )
70 3 6 2 9 ipcl 
 |-  ( ( W e. PreHil /\ Y e. V /\ Y e. V ) -> ( Y ., Y ) e. K )
71 4 12 12 70 syl3anc 
 |-  ( ph -> ( Y ., Y ) e. K )
72 3 9 clmacl 
 |-  ( ( W e. CMod /\ ( X ., X ) e. K /\ ( Y ., Y ) e. K ) -> ( ( X ., X ) + ( Y ., Y ) ) e. K )
73 25 69 71 72 syl3anc 
 |-  ( ph -> ( ( X ., X ) + ( Y ., Y ) ) e. K )
74 3 9 clmacl 
 |-  ( ( W e. CMod /\ ( X ., Y ) e. K /\ ( Y ., X ) e. K ) -> ( ( X ., Y ) + ( Y ., X ) ) e. K )
75 25 29 32 74 syl3anc 
 |-  ( ph -> ( ( X ., Y ) + ( Y ., X ) ) e. K )
76 3 9 clmsub 
 |-  ( ( W e. CMod /\ ( ( X ., X ) + ( Y ., Y ) ) e. K /\ ( ( X ., Y ) + ( Y ., X ) ) e. K ) -> ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) = ( ( ( X ., X ) + ( Y ., Y ) ) ( -g ` F ) ( ( X ., Y ) + ( Y ., X ) ) ) )
77 25 73 75 76 syl3anc 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) = ( ( ( X ., X ) + ( Y ., Y ) ) ( -g ` F ) ( ( X ., Y ) + ( Y ., X ) ) ) )
78 eqid 
 |-  ( -g ` F ) = ( -g ` F )
79 eqid 
 |-  ( +g ` F ) = ( +g ` F )
80 3 6 2 10 78 79 4 11 12 11 12 ip2subdi 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) = ( ( ( X ., X ) ( +g ` F ) ( Y ., Y ) ) ( -g ` F ) ( ( X ., Y ) ( +g ` F ) ( Y ., X ) ) ) )
81 67 77 80 3eqtr4rd 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) = ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) )
82 81 fveq2d 
 |-  ( ph -> ( abs ` ( ( X .- Y ) ., ( X .- Y ) ) ) = ( abs ` ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) ) )
83 62 82 eqtr3d 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) = ( abs ` ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) ) )
84 27 73 sseldd 
 |-  ( ph -> ( ( X ., X ) + ( Y ., Y ) ) e. CC )
85 84 34 abs2dif2d 
 |-  ( ph -> ( abs ` ( ( ( X ., X ) + ( Y ., Y ) ) - ( ( X ., Y ) + ( Y ., X ) ) ) ) <_ ( ( abs ` ( ( X ., X ) + ( Y ., Y ) ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) )
86 83 85 eqbrtrd 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) <_ ( ( abs ` ( ( X ., X ) + ( Y ., Y ) ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) )
87 21 23 43 48 addge0d 
 |-  ( ph -> 0 <_ ( ( X ., X ) + ( Y ., Y ) ) )
88 24 87 absidd 
 |-  ( ph -> ( abs ` ( ( X ., X ) + ( Y ., Y ) ) ) = ( ( X ., X ) + ( Y ., Y ) ) )
89 88 oveq1d 
 |-  ( ph -> ( ( abs ` ( ( X ., X ) + ( Y ., Y ) ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) = ( ( ( X ., X ) + ( Y ., Y ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) )
90 86 89 breqtrd 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) <_ ( ( ( X ., X ) + ( Y ., Y ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) )
91 30 abscld 
 |-  ( ph -> ( abs ` ( X ., Y ) ) e. RR )
92 remulcl 
 |-  ( ( 2 e. RR /\ ( abs ` ( X ., Y ) ) e. RR ) -> ( 2 x. ( abs ` ( X ., Y ) ) ) e. RR )
93 38 91 92 sylancr 
 |-  ( ph -> ( 2 x. ( abs ` ( X ., Y ) ) ) e. RR )
94 30 33 abstrid 
 |-  ( ph -> ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) <_ ( ( abs ` ( X ., Y ) ) + ( abs ` ( Y ., X ) ) ) )
95 91 recnd 
 |-  ( ph -> ( abs ` ( X ., Y ) ) e. CC )
96 95 2timesd 
 |-  ( ph -> ( 2 x. ( abs ` ( X ., Y ) ) ) = ( ( abs ` ( X ., Y ) ) + ( abs ` ( X ., Y ) ) ) )
97 30 abscjd 
 |-  ( ph -> ( abs ` ( * ` ( X ., Y ) ) ) = ( abs ` ( X ., Y ) ) )
98 3 clmcj 
 |-  ( W e. CMod -> * = ( *r ` F ) )
99 25 98 syl 
 |-  ( ph -> * = ( *r ` F ) )
100 99 fveq1d 
 |-  ( ph -> ( * ` ( X ., Y ) ) = ( ( *r ` F ) ` ( X ., Y ) ) )
101 eqid 
 |-  ( *r ` F ) = ( *r ` F )
102 3 6 2 101 ipcj 
 |-  ( ( W e. PreHil /\ X e. V /\ Y e. V ) -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
103 4 11 12 102 syl3anc 
 |-  ( ph -> ( ( *r ` F ) ` ( X ., Y ) ) = ( Y ., X ) )
104 100 103 eqtrd 
 |-  ( ph -> ( * ` ( X ., Y ) ) = ( Y ., X ) )
105 104 fveq2d 
 |-  ( ph -> ( abs ` ( * ` ( X ., Y ) ) ) = ( abs ` ( Y ., X ) ) )
106 97 105 eqtr3d 
 |-  ( ph -> ( abs ` ( X ., Y ) ) = ( abs ` ( Y ., X ) ) )
107 106 oveq2d 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) + ( abs ` ( X ., Y ) ) ) = ( ( abs ` ( X ., Y ) ) + ( abs ` ( Y ., X ) ) ) )
108 96 107 eqtrd 
 |-  ( ph -> ( 2 x. ( abs ` ( X ., Y ) ) ) = ( ( abs ` ( X ., Y ) ) + ( abs ` ( Y ., X ) ) ) )
109 94 108 breqtrrd 
 |-  ( ph -> ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) <_ ( 2 x. ( abs ` ( X ., Y ) ) ) )
110 eqid 
 |-  ( norm ` G ) = ( norm ` G )
111 eqid 
 |-  ( ( Y ., X ) / ( Y ., Y ) ) = ( ( Y ., X ) / ( Y ., Y ) )
112 1 2 3 4 5 6 7 8 9 110 111 11 12 ipcau2 
 |-  ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( ( norm ` G ) ` X ) x. ( ( norm ` G ) ` Y ) ) )
113 1 110 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ X e. V ) -> ( ( norm ` G ) ` X ) = ( sqrt ` ( X ., X ) ) )
114 15 11 113 syl2anc 
 |-  ( ph -> ( ( norm ` G ) ` X ) = ( sqrt ` ( X ., X ) ) )
115 1 110 2 6 tcphnmval 
 |-  ( ( W e. Grp /\ Y e. V ) -> ( ( norm ` G ) ` Y ) = ( sqrt ` ( Y ., Y ) ) )
116 15 12 115 syl2anc 
 |-  ( ph -> ( ( norm ` G ) ` Y ) = ( sqrt ` ( Y ., Y ) ) )
117 114 116 oveq12d 
 |-  ( ph -> ( ( ( norm ` G ) ` X ) x. ( ( norm ` G ) ` Y ) ) = ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
118 112 117 breqtrd 
 |-  ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) )
119 38 a1i 
 |-  ( ph -> 2 e. RR )
120 2pos 
 |-  0 < 2
121 120 a1i 
 |-  ( ph -> 0 < 2 )
122 lemul2 
 |-  ( ( ( abs ` ( X ., Y ) ) e. RR /\ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( abs ` ( X ., Y ) ) <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) <-> ( 2 x. ( abs ` ( X ., Y ) ) ) <_ ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) )
123 91 50 119 121 122 syl112anc 
 |-  ( ph -> ( ( abs ` ( X ., Y ) ) <_ ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) <-> ( 2 x. ( abs ` ( X ., Y ) ) ) <_ ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) )
124 118 123 mpbid 
 |-  ( ph -> ( 2 x. ( abs ` ( X ., Y ) ) ) <_ ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) )
125 35 93 52 109 124 letrd 
 |-  ( ph -> ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) <_ ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) )
126 35 52 24 125 leadd2dd 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) <_ ( ( ( X ., X ) + ( Y ., Y ) ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) )
127 126 55 breqtrrd 
 |-  ( ph -> ( ( ( X ., X ) + ( Y ., Y ) ) + ( abs ` ( ( X ., Y ) + ( Y ., X ) ) ) ) <_ ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) )
128 19 36 57 90 127 letrd 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) <_ ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) )
129 19 recnd 
 |-  ( ph -> ( ( X .- Y ) ., ( X .- Y ) ) e. CC )
130 129 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) ^ 2 ) = ( ( X .- Y ) ., ( X .- Y ) ) )
131 37 sqrtcld 
 |-  ( ph -> ( sqrt ` ( X ., X ) ) e. CC )
132 49 recnd 
 |-  ( ph -> ( sqrt ` ( Y ., Y ) ) e. CC )
133 binom2 
 |-  ( ( ( sqrt ` ( X ., X ) ) e. CC /\ ( sqrt ` ( Y ., Y ) ) e. CC ) -> ( ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) = ( ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) ) )
134 131 132 133 syl2anc 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) = ( ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) ) )
135 37 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( X ., X ) ) ^ 2 ) = ( X ., X ) )
136 135 oveq1d 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) = ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) )
137 54 sqsqrtd 
 |-  ( ph -> ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) = ( Y ., Y ) )
138 136 137 oveq12d 
 |-  ( ph -> ( ( ( ( sqrt ` ( X ., X ) ) ^ 2 ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( ( sqrt ` ( Y ., Y ) ) ^ 2 ) ) = ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) )
139 134 138 eqtrd 
 |-  ( ph -> ( ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) = ( ( ( X ., X ) + ( 2 x. ( ( sqrt ` ( X ., X ) ) x. ( sqrt ` ( Y ., Y ) ) ) ) ) + ( Y ., Y ) ) )
140 128 130 139 3brtr4d 
 |-  ( ph -> ( ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) ^ 2 ) <_ ( ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) )
141 19 61 resqrtcld 
 |-  ( ph -> ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) e. RR )
142 44 49 readdcld 
 |-  ( ph -> ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) e. RR )
143 19 61 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) )
144 21 43 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( X ., X ) ) )
145 23 48 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( Y ., Y ) ) )
146 44 49 144 145 addge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) )
147 141 142 143 146 le2sqd 
 |-  ( ph -> ( ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) <_ ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) <-> ( ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) ^ 2 ) <_ ( ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) ^ 2 ) ) )
148 140 147 mpbird 
 |-  ( ph -> ( sqrt ` ( ( X .- Y ) ., ( X .- Y ) ) ) <_ ( ( sqrt ` ( X ., X ) ) + ( sqrt ` ( Y ., Y ) ) ) )