Proof of Theorem ipcau2
Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑌 = (0g‘𝑊) → (𝑋 , 𝑌) = (𝑋 , (0g‘𝑊))) |
2 | 1 | oveq1d 6564 |
. . . . . 6
⊢ (𝑌 = (0g‘𝑊) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) = ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋))) |
3 | 2 | breq1d 4593 |
. . . . 5
⊢ (𝑌 = (0g‘𝑊) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)) ↔ ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) |
4 | | tchval.n |
. . . . . . . . . . . . 13
⊢ 𝐺 = (toℂHil‘𝑊) |
5 | | tchcph.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑊) |
6 | | tchcph.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = (Scalar‘𝑊) |
7 | | tchcph.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ PreHil) |
8 | | tchcph.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 = (ℂfld
↾s 𝐾)) |
9 | 4, 5, 6, 7, 8 | tchclm 22839 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ ℂMod) |
10 | | tchcph.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = (Base‘𝐹) |
11 | 6, 10 | clmsscn 22687 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆
ℂ) |
12 | 9, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ⊆ ℂ) |
13 | | ipcau2.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
14 | | ipcau2.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
15 | | tchcph.h |
. . . . . . . . . . . . 13
⊢ , =
(·𝑖‘𝑊) |
16 | 6, 15, 5, 10 | ipcl 19797 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 , 𝑌) ∈ 𝐾) |
17 | 7, 13, 14, 16 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 , 𝑌) ∈ 𝐾) |
18 | 12, 17 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 , 𝑌) ∈ ℂ) |
19 | 18 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑌) ∈ ℂ) |
20 | 6, 15, 5, 10 | ipcl 19797 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑌 , 𝑋) ∈ 𝐾) |
21 | 7, 14, 13, 20 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 , 𝑋) ∈ 𝐾) |
22 | 12, 21 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 , 𝑋) ∈ ℂ) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑋) ∈ ℂ) |
24 | 4, 5, 6, 7, 8, 15 | tchcphlem3 22840 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ ℝ) |
25 | 14, 24 | mpdan 699 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℝ) |
26 | 25 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℂ) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ ℂ) |
28 | 6 | clm0 22680 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘𝐹)) |
29 | 9, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 =
(0g‘𝐹)) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 , 𝑌) = 0 ↔ (𝑌 , 𝑌) = (0g‘𝐹))) |
31 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐹) = (0g‘𝐹) |
32 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑊) = (0g‘𝑊) |
33 | 6, 15, 5, 31, 32 | ipeq0 19802 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉) → ((𝑌 , 𝑌) = (0g‘𝐹) ↔ 𝑌 = (0g‘𝑊))) |
34 | 7, 14, 33 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 , 𝑌) = (0g‘𝐹) ↔ 𝑌 = (0g‘𝑊))) |
35 | 30, 34 | bitrd 267 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 , 𝑌) = 0 ↔ 𝑌 = (0g‘𝑊))) |
36 | 35 | necon3bid 2826 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑌 , 𝑌) ≠ 0 ↔ 𝑌 ≠ (0g‘𝑊))) |
37 | 36 | biimpar 501 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ≠ 0) |
38 | 19, 23, 27, 37 | divassd 10715 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))) |
39 | | ipcau2.c |
. . . . . . . . 9
⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌)) |
40 | 39 | oveq2i 6560 |
. . . . . . . 8
⊢ ((𝑋 , 𝑌) · 𝐶) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) |
41 | 38, 40 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · 𝐶)) |
42 | | phllmod 19794 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
43 | 7, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ LMod) |
44 | 43 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ LMod) |
45 | 13 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑋 ∈ 𝑉) |
46 | 39 | fveq2i 6106 |
. . . . . . . . . . . . . . 15
⊢
(∗‘𝐶) =
(∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) |
47 | 23, 27, 37 | cjdivd 13811 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌)))) |
48 | 46, 47 | syl5eq 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌)))) |
49 | 8 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(*𝑟‘𝐹) =
(*𝑟‘(ℂfld ↾s 𝐾))) |
50 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Base‘𝐹)
∈ V |
51 | 10, 50 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐾 ∈ V |
52 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(ℂfld ↾s 𝐾) = (ℂfld
↾s 𝐾) |
53 | | cnfldcj 19574 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∗
= (*𝑟‘ℂfld) |
54 | 52, 53 | ressstarv 15830 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 ∈ V → ∗ =
(*𝑟‘(ℂfld ↾s 𝐾))) |
55 | 51, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∗
= (*𝑟‘(ℂfld ↾s 𝐾)) |
56 | 49, 55 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(*𝑟‘𝐹) = ∗) |
57 | 56 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (∗‘(𝑋 , 𝑌))) |
58 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(*𝑟‘𝐹) = (*𝑟‘𝐹) |
59 | 6, 15, 5, 58 | ipcj 19798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
60 | 7, 13, 14, 59 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
61 | 57, 60 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) |
63 | 62 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(∗‘(∗‘(𝑋 , 𝑌))) = (∗‘(𝑌 , 𝑋))) |
64 | 19 | cjcjd 13787 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(∗‘(∗‘(𝑋 , 𝑌))) = (𝑋 , 𝑌)) |
65 | 63, 64 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑌 , 𝑋)) = (𝑋 , 𝑌)) |
66 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ ℝ) |
67 | 66 | cjred 13814 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑌 , 𝑌)) = (𝑌 , 𝑌)) |
68 | 65, 67 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))) = ((𝑋 , 𝑌) / (𝑌 , 𝑌))) |
69 | 19, 27, 37 | divrecd 10683 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌)))) |
70 | 48, 68, 69 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌)))) |
71 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ ℂMod) |
72 | 17 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑌) ∈ 𝐾) |
73 | 6, 15, 5, 10 | ipcl 19797 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ 𝐾) |
74 | 7, 14, 14, 73 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 , 𝑌) ∈ 𝐾) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ 𝐾) |
76 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐹 = (ℂfld
↾s 𝐾)) |
77 | | phllvec 19793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) |
78 | 7, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ LVec) |
79 | 6 | lvecdrng 18926 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ LVec → 𝐹 ∈
DivRing) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ DivRing) |
81 | 80 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐹 ∈ DivRing) |
82 | 10, 76, 81 | cphreccllem 22786 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑌 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑌) ≠ 0) → (1 / (𝑌 , 𝑌)) ∈ 𝐾) |
83 | 75, 37, 82 | mpd3an23 1418 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (1 / (𝑌 , 𝑌)) ∈ 𝐾) |
84 | 6, 10 | clmmcl 22693 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) |
85 | 71, 72, 83, 84 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) |
86 | 70, 85 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) ∈ 𝐾) |
87 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑌 ∈ 𝑉) |
88 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
89 | 5, 6, 88, 10 | lmodvscl 18703 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧
(∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉) → ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
90 | 44, 86, 87, 89 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) |
91 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(-g‘𝑊) = (-g‘𝑊) |
92 | 5, 91 | lmodvsubcl 18731 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) → (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∈ 𝑉) |
93 | 44, 45, 90, 92 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∈ 𝑉) |
94 | | tchcph.4 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) |
95 | 94 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥)) |
96 | 95 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥)) |
97 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∧ 𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) → (𝑥 , 𝑥) = ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) |
98 | 97 | anidms 675 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) → (𝑥 , 𝑥) = ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) |
99 | 98 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))))) |
100 | 99 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((𝑋(-g‘𝑊)((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))))) |
101 | 93, 96, 100 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) |
102 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(-g‘𝐹) = (-g‘𝐹) |
103 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘𝐹) = (+g‘𝐹) |
104 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ PreHil) |
105 | 6, 15, 5, 91, 102, 103, 104, 45, 90, 45, 90 | ip2subdi 19808 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) = (((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))(-g‘𝐹)((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋)))) |
106 | 76 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (+g‘𝐹) =
(+g‘(ℂfld ↾s 𝐾))) |
107 | | cnfldadd 19572 |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘ℂfld) |
108 | 52, 107 | ressplusg 15818 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ V → + =
(+g‘(ℂfld ↾s 𝐾))) |
109 | 51, 108 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ + =
(+g‘(ℂfld ↾s 𝐾)) |
110 | 106, 109 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (+g‘𝐹) = + ) |
111 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) = (𝑋 , 𝑋)) |
112 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(.r‘𝐹) = (.r‘𝐹) |
113 | 6, 15, 5, 10, 88, 112 | ipass 19809 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧
((∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉 ∧ ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))) |
114 | 104, 86, 87, 90, 113 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))) |
115 | 76 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (.r‘𝐹) =
(.r‘(ℂfld ↾s 𝐾))) |
116 | | cnfldmul 19573 |
. . . . . . . . . . . . . . . . 17
⊢ ·
= (.r‘ℂfld) |
117 | 52, 116 | ressmulr 15829 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ V → · =
(.r‘(ℂfld ↾s 𝐾))) |
118 | 51, 117 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ·
= (.r‘(ℂfld ↾s 𝐾)) |
119 | 115, 118 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (.r‘𝐹) = · ) |
120 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = (∗‘𝐶)) |
121 | 23, 27, 37 | divrecd 10683 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌)))) |
122 | 39, 121 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐶 = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌)))) |
123 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑋) ∈ 𝐾) |
124 | 6, 10 | clmmcl 22693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ ℂMod ∧ (𝑌 , 𝑋) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) |
125 | 71, 123, 83, 124 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) |
126 | 122, 125 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐶 ∈ 𝐾) |
127 | 6, 15, 5, 10, 88, 112, 58 | ipassr2 19811 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ PreHil ∧ (𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) |
128 | 104, 87, 87, 126, 127 | syl13anc 1320 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) |
129 | 119 | oveqd 6566 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = ((𝑌 , 𝑌) · 𝐶)) |
130 | 39 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 , 𝑌) · 𝐶) = ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) |
131 | 23, 27, 37 | divcan2d 10682 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) = (𝑌 , 𝑋)) |
132 | 130, 131 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌) · 𝐶) = (𝑌 , 𝑋)) |
133 | 129, 132 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 , 𝑋)) |
134 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (*𝑟‘𝐹) = ∗) |
135 | 134 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
((*𝑟‘𝐹)‘𝐶) = (∗‘𝐶)) |
136 | 135 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌) = ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) |
137 | 136 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌)) = (𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) |
138 | 128, 133,
137 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = (𝑌 , 𝑋)) |
139 | 119, 120,
138 | oveq123d 6570 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) = ((∗‘𝐶) · (𝑌 , 𝑋))) |
140 | 114, 139 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶) · (𝑌 , 𝑋))) |
141 | 110, 111,
140 | oveq123d 6570 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) = ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))) |
142 | 6, 15, 5, 10, 88, 112, 58 | ipassr2 19811 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) |
143 | 104, 45, 87, 126, 142 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) |
144 | 119 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = ((𝑋 , 𝑌) · 𝐶)) |
145 | 136 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌)) = (𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) |
146 | 143, 144,
145 | 3eqtr3rd 2653 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((𝑋 , 𝑌) · 𝐶)) |
147 | 6, 15, 5, 10, 88, 112 | ipass 19809 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧
((∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋))) |
148 | 104, 86, 87, 45, 147 | syl13anc 1320 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋))) |
149 | 119 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋)) = ((∗‘𝐶) · (𝑌 , 𝑋))) |
150 | 148, 149 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶) · (𝑌 , 𝑋))) |
151 | 110, 146,
150 | oveq123d 6570 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋)) = (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) |
152 | 141, 151 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))(-g‘𝐹)((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) |
153 | 6, 15, 5, 10 | ipcl 19797 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ 𝐾) |
154 | 104, 45, 45, 153 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ 𝐾) |
155 | 6, 10 | clmmcl 22693 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧
(∗‘𝐶) ∈
𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) |
156 | 71, 86, 123, 155 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) |
157 | 6, 10 | clmacl 22692 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) |
158 | 71, 154, 156, 157 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) |
159 | 6, 10 | clmmcl 22693 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾) |
160 | 71, 72, 126, 159 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾) |
161 | 6, 10 | clmacl 22692 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) |
162 | 71, 160, 156, 161 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) |
163 | 6, 10 | clmsub 22688 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾 ∧ (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) |
164 | 71, 158, 162, 163 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) |
165 | 4, 5, 6, 7, 8, 15 | tchcphlem3 22840 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ) |
166 | 13, 165 | mpdan 699 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℝ) |
167 | 166 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℂ) |
168 | 167 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ ℂ) |
169 | 18 | absvalsqd 14029 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌)))) |
170 | 61 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))) = ((𝑋 , 𝑌) · (𝑌 , 𝑋))) |
171 | 169, 170 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (𝑌 , 𝑋))) |
172 | 18 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ) |
173 | 172 | resqcld 12897 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ∈ ℝ) |
174 | 171, 173 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ) |
175 | 174 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ) |
176 | 175, 66, 37 | redivcld 10732 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ∈ ℝ) |
177 | 41, 176 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℝ) |
178 | 177 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℂ) |
179 | 71, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐾 ⊆ ℂ) |
180 | 179, 156 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ ℂ) |
181 | 168, 178,
180 | pnpcan2d 10309 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) |
182 | 164, 181 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) |
183 | 105, 152,
182 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) |
184 | 101, 183 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) |
185 | 166 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ ℝ) |
186 | 185, 177 | subge0d 10496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)) ↔ ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋))) |
187 | 184, 186 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋)) |
188 | 41, 187 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋)) |
189 | | oveq12 6558 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑌 ∧ 𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌)) |
190 | 189 | anidms 675 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌)) |
191 | 190 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌))) |
192 | 191 | rspcv 3278 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑌 , 𝑌))) |
193 | 14, 95, 192 | sylc 63 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑌 , 𝑌)) |
194 | 193 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ (𝑌 , 𝑌)) |
195 | 66, 194, 37 | ne0gt0d 10053 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 < (𝑌 , 𝑌)) |
196 | | ledivmul2 10781 |
. . . . . . 7
⊢ ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ ∧ (𝑋 , 𝑋) ∈ ℝ ∧ ((𝑌 , 𝑌) ∈ ℝ ∧ 0 < (𝑌 , 𝑌))) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) |
197 | 175, 185,
66, 195, 196 | syl112anc 1322 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) |
198 | 188, 197 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
199 | 6, 15, 5, 31, 32 | ip0r 19801 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉) → (𝑋 , (0g‘𝑊)) = (0g‘𝐹)) |
200 | 7, 13, 199 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 , (0g‘𝑊)) = (0g‘𝐹)) |
201 | 200, 29 | eqtr4d 2647 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 , (0g‘𝑊)) = 0) |
202 | 201 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) = (0 · (𝑌 , 𝑋))) |
203 | 22 | mul02d 10113 |
. . . . . . 7
⊢ (𝜑 → (0 · (𝑌 , 𝑋)) = 0) |
204 | 202, 203 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) = 0) |
205 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋)) |
206 | 205 | anidms 675 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋)) |
207 | 206 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋))) |
208 | 207 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑋 , 𝑋))) |
209 | 13, 95, 208 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 , 𝑋)) |
210 | 166, 25, 209, 193 | mulge0d 10483 |
. . . . . 6
⊢ (𝜑 → 0 ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
211 | 204, 210 | eqbrtrd 4605 |
. . . . 5
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
212 | 3, 198, 211 | pm2.61ne 2867 |
. . . 4
⊢ (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
213 | 166, 209 | resqrtcld 14004 |
. . . . . . 7
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ) |
214 | 213 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ) |
215 | 25, 193 | resqrtcld 14004 |
. . . . . . 7
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ) |
216 | 215 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ) |
217 | 214, 216 | sqmuld 12882 |
. . . . 5
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2))) |
218 | 167 | sqsqrtd 14026 |
. . . . . 6
⊢ (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋)) |
219 | 26 | sqsqrtd 14026 |
. . . . . 6
⊢ (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌)) |
220 | 218, 219 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)) = ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
221 | 217, 220 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = ((𝑋 , 𝑋) · (𝑌 , 𝑌))) |
222 | 212, 171,
221 | 3brtr4d 4615 |
. . 3
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2)) |
223 | 213, 215 | remulcld 9949 |
. . . 4
⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ) |
224 | 18 | absge0d 14031 |
. . . 4
⊢ (𝜑 → 0 ≤ (abs‘(𝑋 , 𝑌))) |
225 | 166, 209 | sqrtge0d 14007 |
. . . . 5
⊢ (𝜑 → 0 ≤
(√‘(𝑋 , 𝑋))) |
226 | 25, 193 | sqrtge0d 14007 |
. . . . 5
⊢ (𝜑 → 0 ≤
(√‘(𝑌 , 𝑌))) |
227 | 213, 215,
225, 226 | mulge0d 10483 |
. . . 4
⊢ (𝜑 → 0 ≤
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌)))) |
228 | 172, 223,
224, 227 | le2sqd 12906 |
. . 3
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2))) |
229 | 222, 228 | mpbird 246 |
. 2
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) |
230 | | lmodgrp 18693 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
231 | 43, 230 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ Grp) |
232 | | ipcau2.n |
. . . . 5
⊢ 𝑁 = (norm‘𝐺) |
233 | 4, 232, 5, 15 | tchnmval 22836 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) |
234 | 231, 13, 233 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) |
235 | 4, 232, 5, 15 | tchnmval 22836 |
. . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → (𝑁‘𝑌) = (√‘(𝑌 , 𝑌))) |
236 | 231, 14, 235 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑁‘𝑌) = (√‘(𝑌 , 𝑌))) |
237 | 234, 236 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) |
238 | 229, 237 | breqtrrd 4611 |
1
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) |