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=toCPreHilW
tcphcph.v V=BaseW
tcphcph.f F=ScalarW
tcphcph.1 φWPreHil
tcphcph.2 φF=fld𝑠K
tcphcph.h ,˙=𝑖W
tcphcph.3 φxKx0xxK
tcphcph.4 φxV0x,˙x
tcphcph.k K=BaseF
tcphcph.m -˙=-W
tcphcphlem1.3 φXV
tcphcphlem1.4 φYV
Assertion tcphcphlem1 φX-˙Y,˙X-˙YX,˙X+Y,˙Y

Proof

Step Hyp Ref Expression
1 tcphval.n G=toCPreHilW
2 tcphcph.v V=BaseW
3 tcphcph.f F=ScalarW
4 tcphcph.1 φWPreHil
5 tcphcph.2 φF=fld𝑠K
6 tcphcph.h ,˙=𝑖W
7 tcphcph.3 φxKx0xxK
8 tcphcph.4 φxV0x,˙x
9 tcphcph.k K=BaseF
10 tcphcph.m -˙=-W
11 tcphcphlem1.3 φXV
12 tcphcphlem1.4 φYV
13 phllmod WPreHilWLMod
14 lmodgrp WLModWGrp
15 4 13 14 3syl φWGrp
16 2 10 grpsubcl WGrpXVYVX-˙YV
17 15 11 12 16 syl3anc φX-˙YV
18 1 2 3 4 5 6 tcphcphlem3 φX-˙YVX-˙Y,˙X-˙Y
19 17 18 mpdan φX-˙Y,˙X-˙Y
20 1 2 3 4 5 6 tcphcphlem3 φXVX,˙X
21 11 20 mpdan φX,˙X
22 1 2 3 4 5 6 tcphcphlem3 φYVY,˙Y
23 12 22 mpdan φY,˙Y
24 21 23 readdcld φX,˙X+Y,˙Y
25 1 2 3 4 5 phclm φWCMod
26 3 9 clmsscn WCModK
27 25 26 syl φK
28 3 6 2 9 ipcl WPreHilXVYVX,˙YK
29 4 11 12 28 syl3anc φX,˙YK
30 27 29 sseldd φX,˙Y
31 3 6 2 9 ipcl WPreHilYVXVY,˙XK
32 4 12 11 31 syl3anc φY,˙XK
33 27 32 sseldd φY,˙X
34 30 33 addcld φX,˙Y+Y,˙X
35 34 abscld φX,˙Y+Y,˙X
36 24 35 readdcld φX,˙X+Y,˙Y+X,˙Y+Y,˙X
37 21 recnd φX,˙X
38 2re 2
39 oveq12 x=Xx=Xx,˙x=X,˙X
40 39 anidms x=Xx,˙x=X,˙X
41 40 breq2d x=X0x,˙x0X,˙X
42 8 ralrimiva φxV0x,˙x
43 41 42 11 rspcdva φ0X,˙X
44 21 43 resqrtcld φX,˙X
45 oveq12 x=Yx=Yx,˙x=Y,˙Y
46 45 anidms x=Yx,˙x=Y,˙Y
47 46 breq2d x=Y0x,˙x0Y,˙Y
48 47 42 12 rspcdva φ0Y,˙Y
49 23 48 resqrtcld φY,˙Y
50 44 49 remulcld φX,˙XY,˙Y
51 remulcl 2X,˙XY,˙Y2X,˙XY,˙Y
52 38 50 51 sylancr φ2X,˙XY,˙Y
53 52 recnd φ2X,˙XY,˙Y
54 23 recnd φY,˙Y
55 37 53 54 add32d φX,˙X+2X,˙XY,˙Y+Y,˙Y=X,˙X+Y,˙Y+2X,˙XY,˙Y
56 24 52 readdcld φX,˙X+Y,˙Y+2X,˙XY,˙Y
57 55 56 eqeltrd φX,˙X+2X,˙XY,˙Y+Y,˙Y
58 oveq12 x=X-˙Yx=X-˙Yx,˙x=X-˙Y,˙X-˙Y
59 58 anidms x=X-˙Yx,˙x=X-˙Y,˙X-˙Y
60 59 breq2d x=X-˙Y0x,˙x0X-˙Y,˙X-˙Y
61 60 42 17 rspcdva φ0X-˙Y,˙X-˙Y
62 19 61 absidd φX-˙Y,˙X-˙Y=X-˙Y,˙X-˙Y
63 3 clmadd WCMod+=+F
64 25 63 syl φ+=+F
65 64 oveqd φX,˙X+Y,˙Y=X,˙X+FY,˙Y
66 64 oveqd φX,˙Y+Y,˙X=X,˙Y+FY,˙X
67 65 66 oveq12d φX,˙X+Y,˙Y-FX,˙Y+Y,˙X=X,˙X+FY,˙Y-FX,˙Y+FY,˙X
68 3 6 2 9 ipcl WPreHilXVXVX,˙XK
69 4 11 11 68 syl3anc φX,˙XK
70 3 6 2 9 ipcl WPreHilYVYVY,˙YK
71 4 12 12 70 syl3anc φY,˙YK
72 3 9 clmacl WCModX,˙XKY,˙YKX,˙X+Y,˙YK
73 25 69 71 72 syl3anc φX,˙X+Y,˙YK
74 3 9 clmacl WCModX,˙YKY,˙XKX,˙Y+Y,˙XK
75 25 29 32 74 syl3anc φX,˙Y+Y,˙XK
76 3 9 clmsub WCModX,˙X+Y,˙YKX,˙Y+Y,˙XKX,˙X+Y,˙Y-X,˙Y+Y,˙X=X,˙X+Y,˙Y-FX,˙Y+Y,˙X
77 25 73 75 76 syl3anc φX,˙X+Y,˙Y-X,˙Y+Y,˙X=X,˙X+Y,˙Y-FX,˙Y+Y,˙X
78 eqid -F=-F
79 eqid +F=+F
80 3 6 2 10 78 79 4 11 12 11 12 ip2subdi φX-˙Y,˙X-˙Y=X,˙X+FY,˙Y-FX,˙Y+FY,˙X
81 67 77 80 3eqtr4rd φX-˙Y,˙X-˙Y=X,˙X+Y,˙Y-X,˙Y+Y,˙X
82 81 fveq2d φX-˙Y,˙X-˙Y=X,˙X+Y,˙Y-X,˙Y+Y,˙X
83 62 82 eqtr3d φX-˙Y,˙X-˙Y=X,˙X+Y,˙Y-X,˙Y+Y,˙X
84 27 73 sseldd φX,˙X+Y,˙Y
85 84 34 abs2dif2d φX,˙X+Y,˙Y-X,˙Y+Y,˙XX,˙X+Y,˙Y+X,˙Y+Y,˙X
86 83 85 eqbrtrd φX-˙Y,˙X-˙YX,˙X+Y,˙Y+X,˙Y+Y,˙X
87 21 23 43 48 addge0d φ0X,˙X+Y,˙Y
88 24 87 absidd φX,˙X+Y,˙Y=X,˙X+Y,˙Y
89 88 oveq1d φX,˙X+Y,˙Y+X,˙Y+Y,˙X=X,˙X+Y,˙Y+X,˙Y+Y,˙X
90 86 89 breqtrd φX-˙Y,˙X-˙YX,˙X+Y,˙Y+X,˙Y+Y,˙X
91 30 abscld φX,˙Y
92 remulcl 2X,˙Y2X,˙Y
93 38 91 92 sylancr φ2X,˙Y
94 30 33 abstrid φX,˙Y+Y,˙XX,˙Y+Y,˙X
95 91 recnd φX,˙Y
96 95 2timesd φ2X,˙Y=X,˙Y+X,˙Y
97 30 abscjd φX,˙Y=X,˙Y
98 3 clmcj WCMod*=*F
99 25 98 syl φ*=*F
100 99 fveq1d φX,˙Y=X,˙Y*F
101 eqid *F=*F
102 3 6 2 101 ipcj WPreHilXVYVX,˙Y*F=Y,˙X
103 4 11 12 102 syl3anc φX,˙Y*F=Y,˙X
104 100 103 eqtrd φX,˙Y=Y,˙X
105 104 fveq2d φX,˙Y=Y,˙X
106 97 105 eqtr3d φX,˙Y=Y,˙X
107 106 oveq2d φX,˙Y+X,˙Y=X,˙Y+Y,˙X
108 96 107 eqtrd φ2X,˙Y=X,˙Y+Y,˙X
109 94 108 breqtrrd φX,˙Y+Y,˙X2X,˙Y
110 eqid normG=normG
111 eqid Y,˙XY,˙Y=Y,˙XY,˙Y
112 1 2 3 4 5 6 7 8 9 110 111 11 12 ipcau2 φX,˙YnormGXnormGY
113 1 110 2 6 tcphnmval WGrpXVnormGX=X,˙X
114 15 11 113 syl2anc φnormGX=X,˙X
115 1 110 2 6 tcphnmval WGrpYVnormGY=Y,˙Y
116 15 12 115 syl2anc φnormGY=Y,˙Y
117 114 116 oveq12d φnormGXnormGY=X,˙XY,˙Y
118 112 117 breqtrd φX,˙YX,˙XY,˙Y
119 38 a1i φ2
120 2pos 0<2
121 120 a1i φ0<2
122 lemul2 X,˙YX,˙XY,˙Y20<2X,˙YX,˙XY,˙Y2X,˙Y2X,˙XY,˙Y
123 91 50 119 121 122 syl112anc φX,˙YX,˙XY,˙Y2X,˙Y2X,˙XY,˙Y
124 118 123 mpbid φ2X,˙Y2X,˙XY,˙Y
125 35 93 52 109 124 letrd φX,˙Y+Y,˙X2X,˙XY,˙Y
126 35 52 24 125 leadd2dd φX,˙X+Y,˙Y+X,˙Y+Y,˙XX,˙X+Y,˙Y+2X,˙XY,˙Y
127 126 55 breqtrrd φX,˙X+Y,˙Y+X,˙Y+Y,˙XX,˙X+2X,˙XY,˙Y+Y,˙Y
128 19 36 57 90 127 letrd φX-˙Y,˙X-˙YX,˙X+2X,˙XY,˙Y+Y,˙Y
129 19 recnd φX-˙Y,˙X-˙Y
130 129 sqsqrtd φX-˙Y,˙X-˙Y2=X-˙Y,˙X-˙Y
131 37 sqrtcld φX,˙X
132 49 recnd φY,˙Y
133 binom2 X,˙XY,˙YX,˙X+Y,˙Y2=X,˙X2+2X,˙XY,˙Y+Y,˙Y2
134 131 132 133 syl2anc φX,˙X+Y,˙Y2=X,˙X2+2X,˙XY,˙Y+Y,˙Y2
135 37 sqsqrtd φX,˙X2=X,˙X
136 135 oveq1d φX,˙X2+2X,˙XY,˙Y=X,˙X+2X,˙XY,˙Y
137 54 sqsqrtd φY,˙Y2=Y,˙Y
138 136 137 oveq12d φX,˙X2+2X,˙XY,˙Y+Y,˙Y2=X,˙X+2X,˙XY,˙Y+Y,˙Y
139 134 138 eqtrd φX,˙X+Y,˙Y2=X,˙X+2X,˙XY,˙Y+Y,˙Y
140 128 130 139 3brtr4d φX-˙Y,˙X-˙Y2X,˙X+Y,˙Y2
141 19 61 resqrtcld φX-˙Y,˙X-˙Y
142 44 49 readdcld φX,˙X+Y,˙Y
143 19 61 sqrtge0d φ0X-˙Y,˙X-˙Y
144 21 43 sqrtge0d φ0X,˙X
145 23 48 sqrtge0d φ0Y,˙Y
146 44 49 144 145 addge0d φ0X,˙X+Y,˙Y
147 141 142 143 146 le2sqd φX-˙Y,˙X-˙YX,˙X+Y,˙YX-˙Y,˙X-˙Y2X,˙X+Y,˙Y2
148 140 147 mpbird φX-˙Y,˙X-˙YX,˙X+Y,˙Y