Proof of Theorem tcphcphlem1
Step | Hyp | Ref
| Expression |
1 | | tcphcph.1 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ PreHil) |
2 | | phllmod 20592 |
. . . . . . 7
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
3 | | lmodgrp 19906 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
4 | 1, 2, 3 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ Grp) |
5 | | tcphcphlem1.3 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
6 | | tcphcphlem1.4 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
7 | | tcphcph.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
8 | | tcphcph.m |
. . . . . . 7
⊢ − =
(-g‘𝑊) |
9 | 7, 8 | grpsubcl 18443 |
. . . . . 6
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉) |
10 | 4, 5, 6, 9 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉) |
11 | | tcphval.n |
. . . . . 6
⊢ 𝐺 = (toℂPreHil‘𝑊) |
12 | | tcphcph.f |
. . . . . 6
⊢ 𝐹 = (Scalar‘𝑊) |
13 | | tcphcph.2 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (ℂfld
↾s 𝐾)) |
14 | | tcphcph.h |
. . . . . 6
⊢ , =
(·𝑖‘𝑊) |
15 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24130 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 − 𝑌) ∈ 𝑉) → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℝ) |
16 | 10, 15 | mpdan 687 |
. . . 4
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℝ) |
17 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24130 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ) |
18 | 5, 17 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℝ) |
19 | 11, 7, 12, 1, 13, 14 | tcphcphlem3 24130 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ ℝ) |
20 | 6, 19 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℝ) |
21 | 18, 20 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ ℝ) |
22 | 11, 7, 12, 1, 13 | phclm 24129 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ℂMod) |
23 | | tcphcph.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
24 | 12, 23 | clmsscn 23976 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆
ℂ) |
25 | 22, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ⊆ ℂ) |
26 | 12, 14, 7, 23 | ipcl 20595 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 , 𝑌) ∈ 𝐾) |
27 | 1, 5, 6, 26 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 , 𝑌) ∈ 𝐾) |
28 | 25, 27 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → (𝑋 , 𝑌) ∈ ℂ) |
29 | 12, 14, 7, 23 | ipcl 20595 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑌 , 𝑋) ∈ 𝐾) |
30 | 1, 6, 5, 29 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 , 𝑋) ∈ 𝐾) |
31 | 25, 30 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → (𝑌 , 𝑋) ∈ ℂ) |
32 | 28, 31 | addcld 10852 |
. . . . . 6
⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ ℂ) |
33 | 32 | abscld 15000 |
. . . . 5
⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ∈ ℝ) |
34 | 21, 33 | readdcld 10862 |
. . . 4
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ∈ ℝ) |
35 | 18 | recnd 10861 |
. . . . . 6
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℂ) |
36 | | 2re 11904 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
37 | | oveq12 7222 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋)) |
38 | 37 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋)) |
39 | 38 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋))) |
40 | | tcphcph.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) |
41 | 40 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥)) |
42 | 39, 41, 5 | rspcdva 3539 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑋 , 𝑋)) |
43 | 18, 42 | resqrtcld 14981 |
. . . . . . . . 9
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ) |
44 | | oveq12 7222 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑌 ∧ 𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌)) |
45 | 44 | anidms 570 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌)) |
46 | 45 | breq2d 5065 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌))) |
47 | 46, 41, 6 | rspcdva 3539 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑌 , 𝑌)) |
48 | 20, 47 | resqrtcld 14981 |
. . . . . . . . 9
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ) |
49 | 43, 48 | remulcld 10863 |
. . . . . . . 8
⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ) |
50 | | remulcl 10814 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ) → (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌)))) ∈
ℝ) |
51 | 36, 49, 50 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌)))) ∈
ℝ) |
52 | 51 | recnd 10861 |
. . . . . 6
⊢ (𝜑 → (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌)))) ∈
ℂ) |
53 | 20 | recnd 10861 |
. . . . . 6
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℂ) |
54 | 35, 52, 53 | add32d 11059 |
. . . . 5
⊢ (𝜑 → (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))) |
55 | 21, 51 | readdcld 10862 |
. . . . 5
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) ∈ ℝ) |
56 | 54, 55 | eqeltrd 2838 |
. . . 4
⊢ (𝜑 → (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌)) ∈ ℝ) |
57 | | oveq12 7222 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑋 − 𝑌) ∧ 𝑥 = (𝑋 − 𝑌)) → (𝑥 , 𝑥) = ((𝑋 − 𝑌) , (𝑋 − 𝑌))) |
58 | 57 | anidms 570 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑋 − 𝑌) → (𝑥 , 𝑥) = ((𝑋 − 𝑌) , (𝑋 − 𝑌))) |
59 | 58 | breq2d 5065 |
. . . . . . . . 9
⊢ (𝑥 = (𝑋 − 𝑌) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋 − 𝑌) , (𝑋 − 𝑌)))) |
60 | 59, 41, 10 | rspcdva 3539 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ ((𝑋 − 𝑌) , (𝑋 − 𝑌))) |
61 | 16, 60 | absidd 14986 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) = ((𝑋 − 𝑌) , (𝑋 − 𝑌))) |
62 | 12 | clmadd 23971 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ ℂMod → + =
(+g‘𝐹)) |
63 | 22, 62 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → + =
(+g‘𝐹)) |
64 | 63 | oveqd 7230 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) = ((𝑋 , 𝑋)(+g‘𝐹)(𝑌 , 𝑌))) |
65 | 63 | oveqd 7230 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) = ((𝑋 , 𝑌)(+g‘𝐹)(𝑌 , 𝑋))) |
66 | 64, 65 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋)(+g‘𝐹)(𝑌 , 𝑌))(-g‘𝐹)((𝑋 , 𝑌)(+g‘𝐹)(𝑌 , 𝑋)))) |
67 | 12, 14, 7, 23 | ipcl 20595 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ 𝐾) |
68 | 1, 5, 5, 67 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 , 𝑋) ∈ 𝐾) |
69 | 12, 14, 7, 23 | ipcl 20595 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ 𝐾) |
70 | 1, 6, 6, 69 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 , 𝑌) ∈ 𝐾) |
71 | 12, 23 | clmacl 23981 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ (𝑌 , 𝑌) ∈ 𝐾) → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾) |
72 | 22, 68, 70, 71 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾) |
73 | 12, 23 | clmacl 23981 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾) |
74 | 22, 27, 30, 73 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾) |
75 | 12, 23 | clmsub 23977 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ 𝐾 ∧ ((𝑋 , 𝑌) + (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋)))) |
76 | 22, 72, 74, 75 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌))(-g‘𝐹)((𝑋 , 𝑌) + (𝑌 , 𝑋)))) |
77 | | eqid 2737 |
. . . . . . . . . 10
⊢
(-g‘𝐹) = (-g‘𝐹) |
78 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝐹) = (+g‘𝐹) |
79 | 12, 14, 7, 8, 77, 78, 1, 5, 6,
5, 6 | ip2subdi 20606 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (((𝑋 , 𝑋)(+g‘𝐹)(𝑌 , 𝑌))(-g‘𝐹)((𝑋 , 𝑌)(+g‘𝐹)(𝑌 , 𝑋)))) |
80 | 66, 76, 79 | 3eqtr4rd 2788 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋)))) |
81 | 80 | fveq2d 6721 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) = (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
82 | 61, 81 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) = (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
83 | 25, 72 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 , 𝑋) + (𝑌 , 𝑌)) ∈ ℂ) |
84 | 83, 32 | abs2dif2d 15022 |
. . . . . 6
⊢ (𝜑 → (abs‘(((𝑋 , 𝑋) + (𝑌 , 𝑌)) − ((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
85 | 82, 84 | eqbrtrd 5075 |
. . . . 5
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
86 | 18, 20, 42, 47 | addge0d 11408 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ ((𝑋 , 𝑋) + (𝑌 , 𝑌))) |
87 | 21, 86 | absidd 14986 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) = ((𝑋 , 𝑋) + (𝑌 , 𝑌))) |
88 | 87 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → ((abs‘((𝑋 , 𝑋) + (𝑌 , 𝑌))) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
89 | 85, 88 | breqtrd 5079 |
. . . 4
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))))) |
90 | 28 | abscld 15000 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ) |
91 | | remulcl 10814 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ (abs‘(𝑋 , 𝑌)) ∈ ℝ) → (2 ·
(abs‘(𝑋 , 𝑌))) ∈
ℝ) |
92 | 36, 90, 91 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (2 ·
(abs‘(𝑋 , 𝑌))) ∈
ℝ) |
93 | 28, 31 | abstrid 15020 |
. . . . . . . 8
⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋)))) |
94 | 90 | recnd 10861 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℂ) |
95 | 94 | 2timesd 12073 |
. . . . . . . . 9
⊢ (𝜑 → (2 ·
(abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑋 , 𝑌)))) |
96 | 28 | abscjd 15014 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(∗‘(𝑋 , 𝑌))) = (abs‘(𝑋 , 𝑌))) |
97 | 12 | clmcj 23973 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ ℂMod →
∗ = (*𝑟‘𝐹)) |
98 | 22, 97 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∗ =
(*𝑟‘𝐹)) |
99 | 98 | fveq1d 6719 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = ((*𝑟‘𝐹)‘(𝑋 , 𝑌))) |
100 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
(*𝑟‘𝐹) = (*𝑟‘𝐹) |
101 | 12, 14, 7, 100 | ipcj 20596 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
102 | 1, 5, 6, 101 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
103 | 99, 102 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
104 | 103 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(∗‘(𝑋 , 𝑌))) = (abs‘(𝑌 , 𝑋))) |
105 | 96, 104 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) = (abs‘(𝑌 , 𝑋))) |
106 | 105 | oveq2d 7229 |
. . . . . . . . 9
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋)))) |
107 | 95, 106 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝜑 → (2 ·
(abs‘(𝑋 , 𝑌))) = ((abs‘(𝑋 , 𝑌)) + (abs‘(𝑌 , 𝑋)))) |
108 | 93, 107 | breqtrrd 5081 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ (2 · (abs‘(𝑋 , 𝑌)))) |
109 | | tcphcph.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) |
110 | | eqid 2737 |
. . . . . . . . . 10
⊢
(norm‘𝐺) =
(norm‘𝐺) |
111 | | eqid 2737 |
. . . . . . . . . 10
⊢ ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) / (𝑌 , 𝑌)) |
112 | 11, 7, 12, 1, 13, 14, 109, 40, 23, 110, 111, 5, 6 | ipcau2 24131 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ (((norm‘𝐺)‘𝑋) · ((norm‘𝐺)‘𝑌))) |
113 | 11, 110, 7, 14 | tcphnmval 24126 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → ((norm‘𝐺)‘𝑋) = (√‘(𝑋 , 𝑋))) |
114 | 4, 5, 113 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((norm‘𝐺)‘𝑋) = (√‘(𝑋 , 𝑋))) |
115 | 11, 110, 7, 14 | tcphnmval 24126 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → ((norm‘𝐺)‘𝑌) = (√‘(𝑌 , 𝑌))) |
116 | 4, 6, 115 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((norm‘𝐺)‘𝑌) = (√‘(𝑌 , 𝑌))) |
117 | 114, 116 | oveq12d 7231 |
. . . . . . . . 9
⊢ (𝜑 → (((norm‘𝐺)‘𝑋) · ((norm‘𝐺)‘𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) |
118 | 112, 117 | breqtrd 5079 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) |
119 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 2 ∈
ℝ) |
120 | | 2pos 11933 |
. . . . . . . . . 10
⊢ 0 <
2 |
121 | 120 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 2) |
122 | | lemul2 11685 |
. . . . . . . . 9
⊢
(((abs‘(𝑋
, 𝑌)) ∈ ℝ ∧
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))) ∈ ℝ ∧ (2
∈ ℝ ∧ 0 < 2)) → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ (2 · (abs‘(𝑋 , 𝑌))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))) |
123 | 90, 49, 119, 121, 122 | syl112anc 1376 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ (2 · (abs‘(𝑋 , 𝑌))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))) |
124 | 118, 123 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (2 ·
(abs‘(𝑋 , 𝑌))) ≤ (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))))) |
125 | 33, 92, 51, 108, 124 | letrd 10989 |
. . . . . 6
⊢ (𝜑 → (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋))) ≤ (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) |
126 | 33, 51, 21, 125 | leadd2dd 11447 |
. . . . 5
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))) |
127 | 126, 54 | breqtrrd 5081 |
. . . 4
⊢ (𝜑 → (((𝑋 , 𝑋) + (𝑌 , 𝑌)) + (abs‘((𝑋 , 𝑌) + (𝑌 , 𝑋)))) ≤ (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌))) |
128 | 16, 34, 56, 89, 127 | letrd 10989 |
. . 3
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ≤ (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌))) |
129 | 16 | recnd 10861 |
. . . 4
⊢ (𝜑 → ((𝑋 − 𝑌) , (𝑋 − 𝑌)) ∈ ℂ) |
130 | 129 | sqsqrtd 15003 |
. . 3
⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) = ((𝑋 − 𝑌) , (𝑋 − 𝑌))) |
131 | 35 | sqrtcld 15001 |
. . . . 5
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ) |
132 | 48 | recnd 10861 |
. . . . 5
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ) |
133 | | binom2 13785 |
. . . . 5
⊢
(((√‘(𝑋
, 𝑋)) ∈ ℂ ∧
(√‘(𝑌 , 𝑌)) ∈ ℂ) →
(((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = ((((√‘(𝑋 , 𝑋))↑2) + (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2))) |
134 | 131, 132,
133 | syl2anc 587 |
. . . 4
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = ((((√‘(𝑋 , 𝑋))↑2) + (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2))) |
135 | 35 | sqsqrtd 15003 |
. . . . . 6
⊢ (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋)) |
136 | 135 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → (((√‘(𝑋 , 𝑋))↑2) + (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))))) = ((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))))) |
137 | 53 | sqsqrtd 15003 |
. . . . 5
⊢ (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌)) |
138 | 136, 137 | oveq12d 7231 |
. . . 4
⊢ (𝜑 → ((((√‘(𝑋 , 𝑋))↑2) + (2 ·
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌))))) + ((√‘(𝑌 , 𝑌))↑2)) = (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌))) |
139 | 134, 138 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2) = (((𝑋 , 𝑋) + (2 · ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))) + (𝑌 , 𝑌))) |
140 | 128, 130,
139 | 3brtr4d 5085 |
. 2
⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) ≤ (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2)) |
141 | 16, 60 | resqrtcld 14981 |
. . 3
⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ∈ ℝ) |
142 | 43, 48 | readdcld 10862 |
. . 3
⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))) ∈ ℝ) |
143 | 16, 60 | sqrtge0d 14984 |
. . 3
⊢ (𝜑 → 0 ≤
(√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))) |
144 | 18, 42 | sqrtge0d 14984 |
. . . 4
⊢ (𝜑 → 0 ≤
(√‘(𝑋 , 𝑋))) |
145 | 20, 47 | sqrtge0d 14984 |
. . . 4
⊢ (𝜑 → 0 ≤
(√‘(𝑌 , 𝑌))) |
146 | 43, 48, 144, 145 | addge0d 11408 |
. . 3
⊢ (𝜑 → 0 ≤
((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))) |
147 | 141, 142,
143, 146 | le2sqd 13826 |
. 2
⊢ (𝜑 → ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))) ↔ ((√‘((𝑋 − 𝑌) , (𝑋 − 𝑌)))↑2) ≤ (((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))↑2))) |
148 | 140, 147 | mpbird 260 |
1
⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))) |