This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tcphcphlem1

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

Ref Expression
Hypotheses tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphcph.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
tcphcph.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
tcphcph.1 ⊢ ( 𝜑 → 𝑊 ∈ PreHil )
tcphcph.2 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
tcphcph.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
tcphcph.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ 𝐾 )
tcphcph.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
tcphcph.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
tcphcph.m ⊢ − = ( -g ‘ 𝑊 )
tcphcphlem1.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
tcphcphlem1.4 ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion tcphcphlem1 ( 𝜑 → ( √ ‘ ( ( 𝑋 − 𝑌 ) , ( 𝑋 − 𝑌 ) ) ) ≤ ( ( √ ‘ ( 𝑋 , 𝑋 ) ) + ( √ ‘ ( 𝑌 , 𝑌 ) ) ) )

Proof

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