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 ⊒ ( πœ‘ β†’ ( √ β€˜ ( ( 𝑋 βˆ’ π‘Œ ) , ( 𝑋 βˆ’ π‘Œ ) ) ) ≀ ( ( √ β€˜ ( 𝑋 , 𝑋 ) ) + ( √ β€˜ ( π‘Œ , π‘Œ ) ) ) )