Proof of Theorem ipcau2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑌 = (0g‘𝑊) → (𝑋 , 𝑌) = (𝑋 , (0g‘𝑊))) | 
| 2 | 1 | oveq1d 7446 | . . . . . 6
⊢ (𝑌 = (0g‘𝑊) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) = ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋))) | 
| 3 | 2 | breq1d 5153 | . . . . 5
⊢ (𝑌 = (0g‘𝑊) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)) ↔ ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) | 
| 4 |  | tcphval.n | . . . . . . . . . . . . 13
⊢ 𝐺 = (toℂPreHil‘𝑊) | 
| 5 |  | tcphcph.v | . . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑊) | 
| 6 |  | tcphcph.f | . . . . . . . . . . . . 13
⊢ 𝐹 = (Scalar‘𝑊) | 
| 7 |  | tcphcph.1 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ PreHil) | 
| 8 |  | tcphcph.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 = (ℂfld
↾s 𝐾)) | 
| 9 | 4, 5, 6, 7, 8 | phclm 25266 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ ℂMod) | 
| 10 |  | tcphcph.k | . . . . . . . . . . . . 13
⊢ 𝐾 = (Base‘𝐹) | 
| 11 | 6, 10 | clmsscn 25112 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ ℂMod → 𝐾 ⊆
ℂ) | 
| 12 | 9, 11 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ⊆ ℂ) | 
| 13 |  | ipcau2.3 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 14 |  | ipcau2.4 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 15 |  | tcphcph.h | . . . . . . . . . . . . 13
⊢  , =
(·𝑖‘𝑊) | 
| 16 | 6, 15, 5, 10 | ipcl 21651 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 , 𝑌) ∈ 𝐾) | 
| 17 | 7, 13, 14, 16 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 , 𝑌) ∈ 𝐾) | 
| 18 | 12, 17 | sseldd 3984 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 , 𝑌) ∈ ℂ) | 
| 19 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑌) ∈ ℂ) | 
| 20 | 6, 15, 5, 10 | ipcl 21651 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑌 , 𝑋) ∈ 𝐾) | 
| 21 | 7, 14, 13, 20 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 , 𝑋) ∈ 𝐾) | 
| 22 | 12, 21 | sseldd 3984 | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 , 𝑋) ∈ ℂ) | 
| 23 | 22 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑋) ∈ ℂ) | 
| 24 | 4, 5, 6, 7, 8, 15 | tcphcphlem3 25267 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ ℝ) | 
| 25 | 14, 24 | mpdan 687 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℝ) | 
| 26 | 25 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (𝑌 , 𝑌) ∈ ℂ) | 
| 27 | 26 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ ℂ) | 
| 28 | 6 | clm0 25105 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘𝐹)) | 
| 29 | 9, 28 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 =
(0g‘𝐹)) | 
| 30 | 29 | eqeq2d 2748 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 , 𝑌) = 0 ↔ (𝑌 , 𝑌) = (0g‘𝐹))) | 
| 31 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(0g‘𝐹) = (0g‘𝐹) | 
| 32 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 33 | 6, 15, 5, 31, 32 | ipeq0 21656 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉) → ((𝑌 , 𝑌) = (0g‘𝐹) ↔ 𝑌 = (0g‘𝑊))) | 
| 34 | 7, 14, 33 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 , 𝑌) = (0g‘𝐹) ↔ 𝑌 = (0g‘𝑊))) | 
| 35 | 30, 34 | bitrd 279 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 , 𝑌) = 0 ↔ 𝑌 = (0g‘𝑊))) | 
| 36 | 35 | necon3bid 2985 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑌 , 𝑌) ≠ 0 ↔ 𝑌 ≠ (0g‘𝑊))) | 
| 37 | 36 | biimpar 477 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ≠ 0) | 
| 38 | 19, 23, 27, 37 | divassd 12078 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))) | 
| 39 |  | ipcau2.c | . . . . . . . . 9
⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌)) | 
| 40 | 39 | oveq2i 7442 | . . . . . . . 8
⊢ ((𝑋 , 𝑌) · 𝐶) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) | 
| 41 | 38, 40 | eqtr4di 2795 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · 𝐶)) | 
| 42 |  | oveq12 7440 | . . . . . . . . . . . 12
⊢ ((𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∧ 𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) → (𝑥 , 𝑥) = ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) | 
| 43 | 42 | anidms 566 | . . . . . . . . . . 11
⊢ (𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) → (𝑥 , 𝑥) = ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) | 
| 44 | 43 | breq2d 5155 | . . . . . . . . . 10
⊢ (𝑥 = (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))))) | 
| 45 |  | tcphcph.4 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) | 
| 46 | 45 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥)) | 
| 47 | 46 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ∀𝑥 ∈ 𝑉 0 ≤ (𝑥 , 𝑥)) | 
| 48 |  | phllmod 21648 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | 
| 49 | 7, 48 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ LMod) | 
| 51 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑋 ∈ 𝑉) | 
| 52 | 39 | fveq2i 6909 | . . . . . . . . . . . . . . 15
⊢
(∗‘𝐶) =
(∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) | 
| 53 | 23, 27, 37 | cjdivd 15262 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌)))) | 
| 54 | 52, 53 | eqtrid 2789 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌)))) | 
| 55 | 8 | fveq2d 6910 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(*𝑟‘𝐹) =
(*𝑟‘(ℂfld ↾s 𝐾))) | 
| 56 | 10 | fvexi 6920 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐾 ∈ V | 
| 57 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(ℂfld ↾s 𝐾) = (ℂfld
↾s 𝐾) | 
| 58 |  | cnfldcj 21373 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ∗
= (*𝑟‘ℂfld) | 
| 59 | 57, 58 | ressstarv 17352 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 ∈ V → ∗ =
(*𝑟‘(ℂfld ↾s 𝐾))) | 
| 60 | 56, 59 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ∗
= (*𝑟‘(ℂfld ↾s 𝐾)) | 
| 61 | 55, 60 | eqtr4di 2795 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(*𝑟‘𝐹) = ∗) | 
| 62 | 61 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (∗‘(𝑋 , 𝑌))) | 
| 63 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(*𝑟‘𝐹) = (*𝑟‘𝐹) | 
| 64 | 6, 15, 5, 63 | ipcj 21652 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) | 
| 65 | 7, 13, 14, 64 | syl3anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((*𝑟‘𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) | 
| 66 | 62, 65 | eqtr3d 2779 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) | 
| 67 | 66 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋)) | 
| 68 | 67 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(∗‘(∗‘(𝑋 , 𝑌))) = (∗‘(𝑌 , 𝑋))) | 
| 69 | 19 | cjcjd 15238 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(∗‘(∗‘(𝑋 , 𝑌))) = (𝑋 , 𝑌)) | 
| 70 | 68, 69 | eqtr3d 2779 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑌 , 𝑋)) = (𝑋 , 𝑌)) | 
| 71 | 25 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ ℝ) | 
| 72 | 71 | cjred 15265 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘(𝑌 , 𝑌)) = (𝑌 , 𝑌)) | 
| 73 | 70, 72 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))) = ((𝑋 , 𝑌) / (𝑌 , 𝑌))) | 
| 74 | 19, 27, 37 | divrecd 12046 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌)))) | 
| 75 | 54, 73, 74 | 3eqtrd 2781 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌)))) | 
| 76 | 9 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ ℂMod) | 
| 77 | 17 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑌) ∈ 𝐾) | 
| 78 | 6, 15, 5, 10 | ipcl 21651 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ PreHil ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑌 , 𝑌) ∈ 𝐾) | 
| 79 | 7, 14, 14, 78 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑌 , 𝑌) ∈ 𝐾) | 
| 80 | 79 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑌) ∈ 𝐾) | 
| 81 | 8 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐹 = (ℂfld
↾s 𝐾)) | 
| 82 |  | phllvec 21647 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec) | 
| 83 | 7, 82 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑊 ∈ LVec) | 
| 84 | 6 | lvecdrng 21104 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑊 ∈ LVec → 𝐹 ∈
DivRing) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ DivRing) | 
| 86 | 85 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐹 ∈ DivRing) | 
| 87 | 10, 81, 86 | cphreccllem 25212 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) ∧ (𝑌 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑌) ≠ 0) → (1 / (𝑌 , 𝑌)) ∈ 𝐾) | 
| 88 | 80, 37, 87 | mpd3an23 1465 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (1 / (𝑌 , 𝑌)) ∈ 𝐾) | 
| 89 | 6, 10 | clmmcl 25118 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) | 
| 90 | 76, 77, 88, 89 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) | 
| 91 | 75, 90 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) ∈ 𝐾) | 
| 92 | 14 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑌 ∈ 𝑉) | 
| 93 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) | 
| 94 | 5, 6, 93, 10 | lmodvscl 20876 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧
(∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉) → ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) | 
| 95 | 50, 91, 92, 94 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) | 
| 96 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(-g‘𝑊) = (-g‘𝑊) | 
| 97 | 5, 96 | lmodvsubcl 20905 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉) → (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∈ 𝑉) | 
| 98 | 50, 51, 95, 97 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) ∈ 𝑉) | 
| 99 | 44, 47, 98 | rspcdva 3623 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)))) | 
| 100 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(-g‘𝐹) = (-g‘𝐹) | 
| 101 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(+g‘𝐹) = (+g‘𝐹) | 
| 102 | 7 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝑊 ∈ PreHil) | 
| 103 | 6, 15, 5, 96, 100, 101, 102, 51, 95, 51, 95 | ip2subdi 21662 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) = (((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))(-g‘𝐹)((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋)))) | 
| 104 | 81 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (+g‘𝐹) =
(+g‘(ℂfld ↾s 𝐾))) | 
| 105 |  | cnfldadd 21370 | . . . . . . . . . . . . . . 15
⊢  + =
(+g‘ℂfld) | 
| 106 | 57, 105 | ressplusg 17334 | . . . . . . . . . . . . . 14
⊢ (𝐾 ∈ V → + =
(+g‘(ℂfld ↾s 𝐾))) | 
| 107 | 56, 106 | ax-mp 5 | . . . . . . . . . . . . 13
⊢  + =
(+g‘(ℂfld ↾s 𝐾)) | 
| 108 | 104, 107 | eqtr4di 2795 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (+g‘𝐹) = + ) | 
| 109 |  | eqidd 2738 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) = (𝑋 , 𝑋)) | 
| 110 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(.r‘𝐹) = (.r‘𝐹) | 
| 111 | 6, 15, 5, 10, 93, 110 | ipass 21663 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧
((∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉 ∧ ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) ∈ 𝑉)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))) | 
| 112 | 102, 91, 92, 95, 111 | syl13anc 1374 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))) | 
| 113 | 81 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (.r‘𝐹) =
(.r‘(ℂfld ↾s 𝐾))) | 
| 114 |  | cnfldmul 21372 | . . . . . . . . . . . . . . . . 17
⊢  ·
= (.r‘ℂfld) | 
| 115 | 57, 114 | ressmulr 17351 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ V → · =
(.r‘(ℂfld ↾s 𝐾))) | 
| 116 | 56, 115 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢  ·
= (.r‘(ℂfld ↾s 𝐾)) | 
| 117 | 113, 116 | eqtr4di 2795 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (.r‘𝐹) = · ) | 
| 118 |  | eqidd 2738 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (∗‘𝐶) = (∗‘𝐶)) | 
| 119 | 23, 27, 37 | divrecd 12046 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌)))) | 
| 120 | 39, 119 | eqtrid 2789 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐶 = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌)))) | 
| 121 | 21 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , 𝑋) ∈ 𝐾) | 
| 122 | 6, 10 | clmmcl 25118 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ ℂMod ∧ (𝑌 , 𝑋) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) | 
| 123 | 76, 121, 88, 122 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾) | 
| 124 | 120, 123 | eqeltrd 2841 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐶 ∈ 𝐾) | 
| 125 | 6, 15, 5, 10, 93, 110, 63 | ipassr2 21665 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ PreHil ∧ (𝑌 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) | 
| 126 | 102, 92, 92, 124, 125 | syl13anc 1374 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) | 
| 127 | 117 | oveqd 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = ((𝑌 , 𝑌) · 𝐶)) | 
| 128 | 39 | oveq2i 7442 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑌 , 𝑌) · 𝐶) = ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) | 
| 129 | 23, 27, 37 | divcan2d 12045 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) = (𝑌 , 𝑋)) | 
| 130 | 128, 129 | eqtrid 2789 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌) · 𝐶) = (𝑌 , 𝑋)) | 
| 131 | 127, 130 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑌 , 𝑌)(.r‘𝐹)𝐶) = (𝑌 , 𝑋)) | 
| 132 | 61 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (*𝑟‘𝐹) = ∗) | 
| 133 | 132 | fveq1d 6908 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
((*𝑟‘𝐹)‘𝐶) = (∗‘𝐶)) | 
| 134 | 133 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) →
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌) = ((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) | 
| 135 | 134 | oveq2d 7447 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌)) = (𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) | 
| 136 | 126, 131,
135 | 3eqtr3rd 2786 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = (𝑌 , 𝑋)) | 
| 137 | 117, 118,
136 | oveq123d 7452 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)(.r‘𝐹)(𝑌 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) = ((∗‘𝐶) · (𝑌 , 𝑋))) | 
| 138 | 112, 137 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((∗‘𝐶) · (𝑌 , 𝑋))) | 
| 139 | 108, 109,
138 | oveq123d 7452 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) = ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))) | 
| 140 | 6, 15, 5, 10, 93, 110, 63 | ipassr2 21665 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) | 
| 141 | 102, 51, 92, 124, 140 | syl13anc 1374 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌))) | 
| 142 | 117 | oveqd 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌)(.r‘𝐹)𝐶) = ((𝑋 , 𝑌) · 𝐶)) | 
| 143 | 134 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 ,
(((*𝑟‘𝐹)‘𝐶)( ·𝑠
‘𝑊)𝑌)) = (𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))) | 
| 144 | 141, 142,
143 | 3eqtr3rd 2786 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)) = ((𝑋 , 𝑌) · 𝐶)) | 
| 145 | 6, 15, 5, 10, 93, 110 | ipass 21663 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧
((∗‘𝐶) ∈
𝐾 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋))) | 
| 146 | 102, 91, 92, 51, 145 | syl13anc 1374 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋))) | 
| 147 | 117 | oveqd 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶)(.r‘𝐹)(𝑌 , 𝑋)) = ((∗‘𝐶) · (𝑌 , 𝑋))) | 
| 148 | 146, 147 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌) , 𝑋) = ((∗‘𝐶) · (𝑌 , 𝑋))) | 
| 149 | 108, 144,
148 | oveq123d 7452 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋)) = (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) | 
| 150 | 139, 149 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋)(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌)))(-g‘𝐹)((𝑋 , ((∗‘𝐶)(
·𝑠 ‘𝑊)𝑌))(+g‘𝐹)(((∗‘𝐶)( ·𝑠
‘𝑊)𝑌) , 𝑋))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) | 
| 151 | 6, 15, 5, 10 | ipcl 21651 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ 𝐾) | 
| 152 | 102, 51, 51, 151 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ 𝐾) | 
| 153 | 6, 10 | clmmcl 25118 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧
(∗‘𝐶) ∈
𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) | 
| 154 | 76, 91, 121, 153 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) | 
| 155 | 6, 10 | clmacl 25117 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) | 
| 156 | 76, 152, 154, 155 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) | 
| 157 | 6, 10 | clmmcl 25118 | . . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ 𝐶 ∈ 𝐾) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾) | 
| 158 | 76, 77, 124, 157 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾) | 
| 159 | 6, 10 | clmacl 25117 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) | 
| 160 | 76, 158, 154, 159 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) | 
| 161 | 6, 10 | clmsub 25113 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾 ∧ (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) | 
| 162 | 76, 156, 160, 161 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))) | 
| 163 | 4, 5, 6, 7, 8, 15 | tcphcphlem3 25267 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ) | 
| 164 | 13, 163 | mpdan 687 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℝ) | 
| 165 | 164 | recnd 11289 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 , 𝑋) ∈ ℂ) | 
| 166 | 165 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ ℂ) | 
| 167 | 18 | absvalsqd 15481 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌)))) | 
| 168 | 66 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))) = ((𝑋 , 𝑌) · (𝑌 , 𝑋))) | 
| 169 | 167, 168 | eqtrd 2777 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (𝑌 , 𝑋))) | 
| 170 | 18 | abscld 15475 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ) | 
| 171 | 170 | resqcld 14165 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ∈ ℝ) | 
| 172 | 169, 171 | eqeltrrd 2842 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ) | 
| 173 | 172 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ) | 
| 174 | 173, 71, 37 | redivcld 12095 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ∈ ℝ) | 
| 175 | 41, 174 | eqeltrrd 2842 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℝ) | 
| 176 | 175 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℂ) | 
| 177 | 76, 11 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 𝐾 ⊆ ℂ) | 
| 178 | 177, 154 | sseldd 3984 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ ℂ) | 
| 179 | 166, 176,
178 | pnpcan2d 11658 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) | 
| 180 | 162, 179 | eqtr3d 2779 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g‘𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) | 
| 181 | 103, 150,
180 | 3eqtrd 2781 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌)) , (𝑋(-g‘𝑊)((∗‘𝐶)( ·𝑠
‘𝑊)𝑌))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) | 
| 182 | 99, 181 | breqtrd 5169 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶))) | 
| 183 | 164 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (𝑋 , 𝑋) ∈ ℝ) | 
| 184 | 183, 175 | subge0d 11853 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)) ↔ ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋))) | 
| 185 | 182, 184 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋)) | 
| 186 | 41, 185 | eqbrtrd 5165 | . . . . . 6
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋)) | 
| 187 |  | oveq12 7440 | . . . . . . . . . . . 12
⊢ ((𝑥 = 𝑌 ∧ 𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌)) | 
| 188 | 187 | anidms 566 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌)) | 
| 189 | 188 | breq2d 5155 | . . . . . . . . . 10
⊢ (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌))) | 
| 190 | 189, 46, 14 | rspcdva 3623 | . . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑌 , 𝑌)) | 
| 191 | 190 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 ≤ (𝑌 , 𝑌)) | 
| 192 | 71, 191, 37 | ne0gt0d 11398 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → 0 < (𝑌 , 𝑌)) | 
| 193 |  | ledivmul2 12147 | . . . . . . 7
⊢ ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ ∧ (𝑋 , 𝑋) ∈ ℝ ∧ ((𝑌 , 𝑌) ∈ ℝ ∧ 0 < (𝑌 , 𝑌))) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) | 
| 194 | 173, 183,
71, 192, 193 | syl112anc 1376 | . . . . . 6
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))) | 
| 195 | 186, 194 | mpbid 232 | . . . . 5
⊢ ((𝜑 ∧ 𝑌 ≠ (0g‘𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 196 | 6, 15, 5, 31, 32 | ip0r 21655 | . . . . . . . . . 10
⊢ ((𝑊 ∈ PreHil ∧ 𝑋 ∈ 𝑉) → (𝑋 , (0g‘𝑊)) = (0g‘𝐹)) | 
| 197 | 7, 13, 196 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 , (0g‘𝑊)) = (0g‘𝐹)) | 
| 198 | 197, 29 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → (𝑋 , (0g‘𝑊)) = 0) | 
| 199 | 198 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) = (0 · (𝑌 , 𝑋))) | 
| 200 | 22 | mul02d 11459 | . . . . . . 7
⊢ (𝜑 → (0 · (𝑌 , 𝑋)) = 0) | 
| 201 | 199, 200 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) = 0) | 
| 202 |  | oveq12 7440 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋)) | 
| 203 | 202 | anidms 566 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋)) | 
| 204 | 203 | breq2d 5155 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋))) | 
| 205 | 204, 46, 13 | rspcdva 3623 | . . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑋 , 𝑋)) | 
| 206 | 164, 25, 205, 190 | mulge0d 11840 | . . . . . 6
⊢ (𝜑 → 0 ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 207 | 201, 206 | eqbrtrd 5165 | . . . . 5
⊢ (𝜑 → ((𝑋 , (0g‘𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 208 | 3, 195, 207 | pm2.61ne 3027 | . . . 4
⊢ (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 209 | 164, 205 | resqrtcld 15456 | . . . . . . 7
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ) | 
| 210 | 209 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ) | 
| 211 | 25, 190 | resqrtcld 15456 | . . . . . . 7
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ) | 
| 212 | 211 | recnd 11289 | . . . . . 6
⊢ (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ) | 
| 213 | 210, 212 | sqmuld 14198 | . . . . 5
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2))) | 
| 214 | 165 | sqsqrtd 15478 | . . . . . 6
⊢ (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋)) | 
| 215 | 26 | sqsqrtd 15478 | . . . . . 6
⊢ (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌)) | 
| 216 | 214, 215 | oveq12d 7449 | . . . . 5
⊢ (𝜑 → (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)) = ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 217 | 213, 216 | eqtrd 2777 | . . . 4
⊢ (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = ((𝑋 , 𝑋) · (𝑌 , 𝑌))) | 
| 218 | 208, 169,
217 | 3brtr4d 5175 | . . 3
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2)) | 
| 219 | 209, 211 | remulcld 11291 | . . . 4
⊢ (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ) | 
| 220 | 18 | absge0d 15483 | . . . 4
⊢ (𝜑 → 0 ≤ (abs‘(𝑋 , 𝑌))) | 
| 221 | 164, 205 | sqrtge0d 15459 | . . . . 5
⊢ (𝜑 → 0 ≤
(√‘(𝑋 , 𝑋))) | 
| 222 | 25, 190 | sqrtge0d 15459 | . . . . 5
⊢ (𝜑 → 0 ≤
(√‘(𝑌 , 𝑌))) | 
| 223 | 209, 211,
221, 222 | mulge0d 11840 | . . . 4
⊢ (𝜑 → 0 ≤
((√‘(𝑋 , 𝑋)) ·
(√‘(𝑌 , 𝑌)))) | 
| 224 | 170, 219,
220, 223 | le2sqd 14296 | . . 3
⊢ (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2))) | 
| 225 | 218, 224 | mpbird 257 | . 2
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) | 
| 226 |  | lmodgrp 20865 | . . . . 5
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | 
| 227 | 49, 226 | syl 17 | . . . 4
⊢ (𝜑 → 𝑊 ∈ Grp) | 
| 228 |  | ipcau2.n | . . . . 5
⊢ 𝑁 = (norm‘𝐺) | 
| 229 | 4, 228, 5, 15 | tcphnmval 25263 | . . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) | 
| 230 | 227, 13, 229 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) | 
| 231 | 4, 228, 5, 15 | tcphnmval 25263 | . . . 4
⊢ ((𝑊 ∈ Grp ∧ 𝑌 ∈ 𝑉) → (𝑁‘𝑌) = (√‘(𝑌 , 𝑌))) | 
| 232 | 227, 14, 231 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑁‘𝑌) = (√‘(𝑌 , 𝑌))) | 
| 233 | 230, 232 | oveq12d 7449 | . 2
⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))) | 
| 234 | 225, 233 | breqtrrd 5171 | 1
⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) |