MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipcau2 Structured version   Visualization version   GIF version

Theorem ipcau2 23154
Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.)
Hypotheses
Ref Expression
tchval.n 𝐺 = (toℂHil‘𝑊)
tchcph.v 𝑉 = (Base‘𝑊)
tchcph.f 𝐹 = (Scalar‘𝑊)
tchcph.1 (𝜑𝑊 ∈ PreHil)
tchcph.2 (𝜑𝐹 = (ℂflds 𝐾))
tchcph.h , = (·𝑖𝑊)
tchcph.3 ((𝜑 ∧ (𝑥𝐾𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)
tchcph.4 ((𝜑𝑥𝑉) → 0 ≤ (𝑥 , 𝑥))
tchcph.k 𝐾 = (Base‘𝐹)
ipcau2.n 𝑁 = (norm‘𝐺)
ipcau2.c 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌))
ipcau2.3 (𝜑𝑋𝑉)
ipcau2.4 (𝜑𝑌𝑉)
Assertion
Ref Expression
ipcau2 (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁𝑋) · (𝑁𝑌)))
Distinct variable groups:   𝑥, ,   𝑥,𝐹   𝑥,𝐺   𝑥,𝑉   𝑥,𝐶   𝜑,𝑥   𝑥,𝑊   𝑥,𝑋   𝑥,𝑌
Allowed substitution hints:   𝐾(𝑥)   𝑁(𝑥)

Proof of Theorem ipcau2
StepHypRef Expression
1 oveq2 6773 . . . . . . 7 (𝑌 = (0g𝑊) → (𝑋 , 𝑌) = (𝑋 , (0g𝑊)))
21oveq1d 6780 . . . . . 6 (𝑌 = (0g𝑊) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) = ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)))
32breq1d 4770 . . . . 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 (𝜑𝐹 = (ℂflds 𝐾))
94, 5, 6, 7, 8tchclm 23152 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℂMod)
10 tchcph.k . . . . . . . . . . . . 13 𝐾 = (Base‘𝐹)
116, 10clmsscn 23000 . . . . . . . . . . . 12 (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ)
129, 11syl 17 . . . . . . . . . . 11 (𝜑𝐾 ⊆ ℂ)
13 ipcau2.3 . . . . . . . . . . . 12 (𝜑𝑋𝑉)
14 ipcau2.4 . . . . . . . . . . . 12 (𝜑𝑌𝑉)
15 tchcph.h . . . . . . . . . . . . 13 , = (·𝑖𝑊)
166, 15, 5, 10ipcl 20101 . . . . . . . . . . . 12 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉) → (𝑋 , 𝑌) ∈ 𝐾)
177, 13, 14, 16syl3anc 1439 . . . . . . . . . . 11 (𝜑 → (𝑋 , 𝑌) ∈ 𝐾)
1812, 17sseldd 3710 . . . . . . . . . 10 (𝜑 → (𝑋 , 𝑌) ∈ ℂ)
1918adantr 472 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑌) ∈ ℂ)
206, 15, 5, 10ipcl 20101 . . . . . . . . . . . 12 ((𝑊 ∈ PreHil ∧ 𝑌𝑉𝑋𝑉) → (𝑌 , 𝑋) ∈ 𝐾)
217, 14, 13, 20syl3anc 1439 . . . . . . . . . . 11 (𝜑 → (𝑌 , 𝑋) ∈ 𝐾)
2212, 21sseldd 3710 . . . . . . . . . 10 (𝜑 → (𝑌 , 𝑋) ∈ ℂ)
2322adantr 472 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑋) ∈ ℂ)
244, 5, 6, 7, 8, 15tchcphlem3 23153 . . . . . . . . . . . 12 ((𝜑𝑌𝑉) → (𝑌 , 𝑌) ∈ ℝ)
2514, 24mpdan 705 . . . . . . . . . . 11 (𝜑 → (𝑌 , 𝑌) ∈ ℝ)
2625recnd 10181 . . . . . . . . . 10 (𝜑 → (𝑌 , 𝑌) ∈ ℂ)
2726adantr 472 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ ℂ)
286clm0 22993 . . . . . . . . . . . . . 14 (𝑊 ∈ ℂMod → 0 = (0g𝐹))
299, 28syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 = (0g𝐹))
3029eqeq2d 2734 . . . . . . . . . . . 12 (𝜑 → ((𝑌 , 𝑌) = 0 ↔ (𝑌 , 𝑌) = (0g𝐹)))
31 eqid 2724 . . . . . . . . . . . . . 14 (0g𝐹) = (0g𝐹)
32 eqid 2724 . . . . . . . . . . . . . 14 (0g𝑊) = (0g𝑊)
336, 15, 5, 31, 32ipeq0 20106 . . . . . . . . . . . . 13 ((𝑊 ∈ PreHil ∧ 𝑌𝑉) → ((𝑌 , 𝑌) = (0g𝐹) ↔ 𝑌 = (0g𝑊)))
347, 14, 33syl2anc 696 . . . . . . . . . . . 12 (𝜑 → ((𝑌 , 𝑌) = (0g𝐹) ↔ 𝑌 = (0g𝑊)))
3530, 34bitrd 268 . . . . . . . . . . 11 (𝜑 → ((𝑌 , 𝑌) = 0 ↔ 𝑌 = (0g𝑊)))
3635necon3bid 2940 . . . . . . . . . 10 (𝜑 → ((𝑌 , 𝑌) ≠ 0 ↔ 𝑌 ≠ (0g𝑊)))
3736biimpar 503 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ≠ 0)
3819, 23, 27, 37divassd 10949 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))))
39 ipcau2.c . . . . . . . . 9 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌))
4039oveq2i 6776 . . . . . . . 8 ((𝑋 , 𝑌) · 𝐶) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))
4138, 40syl6eqr 2776 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · 𝐶))
42 phllmod 20098 . . . . . . . . . . . . 13 (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
437, 42syl 17 . . . . . . . . . . . 12 (𝜑𝑊 ∈ LMod)
4443adantr 472 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ LMod)
4513adantr 472 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑋𝑉)
4639fveq2i 6307 . . . . . . . . . . . . . . 15 (∗‘𝐶) = (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌)))
4723, 27, 37cjdivd 14083 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))))
4846, 47syl5eq 2770 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))))
498fveq2d 6308 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (*𝑟𝐹) = (*𝑟‘(ℂflds 𝐾)))
50 fvex 6314 . . . . . . . . . . . . . . . . . . . . . . 23 (Base‘𝐹) ∈ V
5110, 50eqeltri 2799 . . . . . . . . . . . . . . . . . . . . . 22 𝐾 ∈ V
52 eqid 2724 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂflds 𝐾) = (ℂflds 𝐾)
53 cnfldcj 19876 . . . . . . . . . . . . . . . . . . . . . . 23 ∗ = (*𝑟‘ℂfld)
5452, 53ressstarv 16130 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ V → ∗ = (*𝑟‘(ℂflds 𝐾)))
5551, 54ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ∗ = (*𝑟‘(ℂflds 𝐾))
5649, 55syl6eqr 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (*𝑟𝐹) = ∗)
5756fveq1d 6306 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (∗‘(𝑋 , 𝑌)))
58 eqid 2724 . . . . . . . . . . . . . . . . . . . . 21 (*𝑟𝐹) = (*𝑟𝐹)
596, 15, 5, 58ipcj 20102 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉) → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
607, 13, 14, 59syl3anc 1439 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6157, 60eqtr3d 2760 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6261adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6362fveq2d 6308 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(∗‘(𝑋 , 𝑌))) = (∗‘(𝑌 , 𝑋)))
6419cjcjd 14059 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(∗‘(𝑋 , 𝑌))) = (𝑋 , 𝑌))
6563, 64eqtr3d 2760 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑌 , 𝑋)) = (𝑋 , 𝑌))
6625adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ ℝ)
6766cjred 14086 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑌 , 𝑌)) = (𝑌 , 𝑌))
6865, 67oveq12d 6783 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))) = ((𝑋 , 𝑌) / (𝑌 , 𝑌)))
6919, 27, 37divrecd 10917 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))))
7048, 68, 693eqtrd 2762 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))))
719adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ ℂMod)
7217adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑌) ∈ 𝐾)
736, 15, 5, 10ipcl 20101 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ PreHil ∧ 𝑌𝑉𝑌𝑉) → (𝑌 , 𝑌) ∈ 𝐾)
747, 14, 14, 73syl3anc 1439 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 , 𝑌) ∈ 𝐾)
7574adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ 𝐾)
768adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐹 = (ℂflds 𝐾))
77 phllvec 20097 . . . . . . . . . . . . . . . . . . 19 (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
787, 77syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ LVec)
796lvecdrng 19228 . . . . . . . . . . . . . . . . . 18 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
8078, 79syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ DivRing)
8180adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐹 ∈ DivRing)
8210, 76, 81cphreccllem 23099 . . . . . . . . . . . . . . 15 (((𝜑𝑌 ≠ (0g𝑊)) ∧ (𝑌 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑌) ≠ 0) → (1 / (𝑌 , 𝑌)) ∈ 𝐾)
8375, 37, 82mpd3an23 1539 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (1 / (𝑌 , 𝑌)) ∈ 𝐾)
846, 10clmmcl 23006 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
8571, 72, 83, 84syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
8670, 85eqeltrd 2803 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) ∈ 𝐾)
8714adantr 472 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑌𝑉)
88 eqid 2724 . . . . . . . . . . . . 13 ( ·𝑠𝑊) = ( ·𝑠𝑊)
895, 6, 88, 10lmodvscl 19003 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ (∗‘𝐶) ∈ 𝐾𝑌𝑉) → ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)
9044, 86, 87, 89syl3anc 1439 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)
91 eqid 2724 . . . . . . . . . . . 12 (-g𝑊) = (-g𝑊)
925, 91lmodvsubcl 19031 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ 𝑋𝑉 ∧ ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉) → (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∈ 𝑉)
9344, 45, 90, 92syl3anc 1439 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∈ 𝑉)
94 tchcph.4 . . . . . . . . . . . 12 ((𝜑𝑥𝑉) → 0 ≤ (𝑥 , 𝑥))
9594ralrimiva 3068 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑉 0 ≤ (𝑥 , 𝑥))
9695adantr 472 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → ∀𝑥𝑉 0 ≤ (𝑥 , 𝑥))
97 oveq12 6774 . . . . . . . . . . . . 13 ((𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∧ 𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) → (𝑥 , 𝑥) = ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
9897anidms 680 . . . . . . . . . . . 12 (𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) → (𝑥 , 𝑥) = ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
9998breq2d 4772 . . . . . . . . . . 11 (𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)))))
10099rspcv 3409 . . . . . . . . . 10 ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∈ 𝑉 → (∀𝑥𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)))))
10193, 96, 100sylc 65 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
102 eqid 2724 . . . . . . . . . . 11 (-g𝐹) = (-g𝐹)
103 eqid 2724 . . . . . . . . . . 11 (+g𝐹) = (+g𝐹)
1047adantr 472 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ PreHil)
1056, 15, 5, 91, 102, 103, 104, 45, 90, 45, 90ip2subdi 20112 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) = (((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))(-g𝐹)((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋))))
10676fveq2d 6308 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (+g𝐹) = (+g‘(ℂflds 𝐾)))
107 cnfldadd 19874 . . . . . . . . . . . . . . 15 + = (+g‘ℂfld)
10852, 107ressplusg 16116 . . . . . . . . . . . . . 14 (𝐾 ∈ V → + = (+g‘(ℂflds 𝐾)))
10951, 108ax-mp 5 . . . . . . . . . . . . 13 + = (+g‘(ℂflds 𝐾))
110106, 109syl6eqr 2776 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (+g𝐹) = + )
111 eqidd 2725 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) = (𝑋 , 𝑋))
112 eqid 2724 . . . . . . . . . . . . . . 15 (.r𝐹) = (.r𝐹)
1136, 15, 5, 10, 88, 112ipass 20113 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ ((∗‘𝐶) ∈ 𝐾𝑌𝑉 ∧ ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))))
114104, 86, 87, 90, 113syl13anc 1441 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))))
11576fveq2d 6308 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (.r𝐹) = (.r‘(ℂflds 𝐾)))
116 cnfldmul 19875 . . . . . . . . . . . . . . . . 17 · = (.r‘ℂfld)
11752, 116ressmulr 16129 . . . . . . . . . . . . . . . 16 (𝐾 ∈ V → · = (.r‘(ℂflds 𝐾)))
11851, 117ax-mp 5 . . . . . . . . . . . . . . 15 · = (.r‘(ℂflds 𝐾))
119115, 118syl6eqr 2776 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (.r𝐹) = · )
120 eqidd 2725 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = (∗‘𝐶))
12123, 27, 37divrecd 10917 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))))
12239, 121syl5eq 2770 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐶 = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))))
12321adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑋) ∈ 𝐾)
1246, 10clmmcl 23006 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ ℂMod ∧ (𝑌 , 𝑋) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
12571, 123, 83, 124syl3anc 1439 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
126122, 125eqeltrd 2803 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐶𝐾)
1276, 15, 5, 10, 88, 112, 58ipassr2 20115 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ PreHil ∧ (𝑌𝑉𝑌𝑉𝐶𝐾)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
128104, 87, 87, 126, 127syl13anc 1441 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
129119oveqd 6782 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = ((𝑌 , 𝑌) · 𝐶))
13039oveq2i 6776 . . . . . . . . . . . . . . . . 17 ((𝑌 , 𝑌) · 𝐶) = ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))
13123, 27, 37divcan2d 10916 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) = (𝑌 , 𝑋))
132130, 131syl5eq 2770 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌) · 𝐶) = (𝑌 , 𝑋))
133129, 132eqtrd 2758 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , 𝑋))
13456adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → (*𝑟𝐹) = ∗)
135134fveq1d 6306 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((*𝑟𝐹)‘𝐶) = (∗‘𝐶))
136135oveq1d 6780 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌) = ((∗‘𝐶)( ·𝑠𝑊)𝑌))
137136oveq2d 6781 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))
138128, 133, 1373eqtr3rd 2767 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑌 , 𝑋))
139119, 120, 138oveq123d 6786 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((∗‘𝐶) · (𝑌 , 𝑋)))
140114, 139eqtrd 2758 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶) · (𝑌 , 𝑋)))
141110, 111, 140oveq123d 6786 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))))
1426, 15, 5, 10, 88, 112, 58ipassr2 20115 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ (𝑋𝑉𝑌𝑉𝐶𝐾)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
143104, 45, 87, 126, 142syl13anc 1441 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
144119oveqd 6782 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = ((𝑋 , 𝑌) · 𝐶))
145136oveq2d 6781 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))
146143, 144, 1453eqtr3rd 2767 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((𝑋 , 𝑌) · 𝐶))
1476, 15, 5, 10, 88, 112ipass 20113 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ ((∗‘𝐶) ∈ 𝐾𝑌𝑉𝑋𝑉)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)))
148104, 86, 87, 45, 147syl13anc 1441 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)))
149119oveqd 6782 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)) = ((∗‘𝐶) · (𝑌 , 𝑋)))
150148, 149eqtrd 2758 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶) · (𝑌 , 𝑋)))
151110, 146, 150oveq123d 6786 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋)) = (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))
152141, 151oveq12d 6783 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))(-g𝐹)((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
1536, 15, 5, 10ipcl 20101 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑋𝑉) → (𝑋 , 𝑋) ∈ 𝐾)
154104, 45, 45, 153syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ 𝐾)
1556, 10clmmcl 23006 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (∗‘𝐶) ∈ 𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾)
15671, 86, 123, 155syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾)
1576, 10clmacl 23005 . . . . . . . . . . . . 13 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
15871, 154, 156, 157syl3anc 1439 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
1596, 10clmmcl 23006 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾𝐶𝐾) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾)
16071, 72, 126, 159syl3anc 1439 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾)
1616, 10clmacl 23005 . . . . . . . . . . . . 13 ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
16271, 160, 156, 161syl3anc 1439 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
1636, 10clmsub 23001 . . . . . . . . . . . 12 ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾 ∧ (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
16471, 158, 162, 163syl3anc 1439 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
1654, 5, 6, 7, 8, 15tchcphlem3 23153 . . . . . . . . . . . . . . 15 ((𝜑𝑋𝑉) → (𝑋 , 𝑋) ∈ ℝ)
16613, 165mpdan 705 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 , 𝑋) ∈ ℝ)
167166recnd 10181 . . . . . . . . . . . . 13 (𝜑 → (𝑋 , 𝑋) ∈ ℂ)
168167adantr 472 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ ℂ)
16918absvalsqd 14301 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))))
17061oveq2d 6781 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))) = ((𝑋 , 𝑌) · (𝑌 , 𝑋)))
171169, 170eqtrd 2758 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (𝑌 , 𝑋)))
17218abscld 14295 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ)
173172resqcld 13150 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ∈ ℝ)
174171, 173eqeltrrd 2804 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ)
175174adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ)
176175, 66, 37redivcld 10966 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ∈ ℝ)
17741, 176eqeltrrd 2804 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℝ)
178177recnd 10181 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℂ)
17971, 11syl 17 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐾 ⊆ ℂ)
180179, 156sseldd 3710 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ ℂ)
181168, 178, 180pnpcan2d 10543 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
182164, 181eqtr3d 2760 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
183105, 152, 1823eqtrd 2762 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
184101, 183breqtrd 4786 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
185166adantr 472 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ ℝ)
186185, 177subge0d 10730 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → (0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)) ↔ ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋)))
187184, 186mpbid 222 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋))
18841, 187eqbrtrd 4782 . . . . . 6 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋))
189 oveq12 6774 . . . . . . . . . . . . 13 ((𝑥 = 𝑌𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌))
190189anidms 680 . . . . . . . . . . . 12 (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌))
191190breq2d 4772 . . . . . . . . . . 11 (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌)))
192191rspcv 3409 . . . . . . . . . 10 (𝑌𝑉 → (∀𝑥𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑌 , 𝑌)))
19314, 95, 192sylc 65 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑌 , 𝑌))
194193adantr 472 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ (𝑌 , 𝑌))
19566, 194, 37ne0gt0d 10287 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → 0 < (𝑌 , 𝑌))
196 ledivmul2 11015 . . . . . . 7 ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ ∧ (𝑋 , 𝑋) ∈ ℝ ∧ ((𝑌 , 𝑌) ∈ ℝ ∧ 0 < (𝑌 , 𝑌))) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))))
197175, 185, 66, 195, 196syl112anc 1443 . . . . . 6 ((𝜑𝑌 ≠ (0g𝑊)) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))))
198188, 197mpbid 222 . . . . 5 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
1996, 15, 5, 31, 32ip0r 20105 . . . . . . . . . 10 ((𝑊 ∈ PreHil ∧ 𝑋𝑉) → (𝑋 , (0g𝑊)) = (0g𝐹))
2007, 13, 199syl2anc 696 . . . . . . . . 9 (𝜑 → (𝑋 , (0g𝑊)) = (0g𝐹))
201200, 29eqtr4d 2761 . . . . . . . 8 (𝜑 → (𝑋 , (0g𝑊)) = 0)
202201oveq1d 6780 . . . . . . 7 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) = (0 · (𝑌 , 𝑋)))
20322mul02d 10347 . . . . . . 7 (𝜑 → (0 · (𝑌 , 𝑋)) = 0)
204202, 203eqtrd 2758 . . . . . 6 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) = 0)
205 oveq12 6774 . . . . . . . . . . 11 ((𝑥 = 𝑋𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋))
206205anidms 680 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋))
207206breq2d 4772 . . . . . . . . 9 (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋)))
208207rspcv 3409 . . . . . . . 8 (𝑋𝑉 → (∀𝑥𝑉 0 ≤ (𝑥 , 𝑥) → 0 ≤ (𝑋 , 𝑋)))
20913, 95, 208sylc 65 . . . . . . 7 (𝜑 → 0 ≤ (𝑋 , 𝑋))
210166, 25, 209, 193mulge0d 10717 . . . . . 6 (𝜑 → 0 ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
211204, 210eqbrtrd 4782 . . . . 5 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
2123, 198, 211pm2.61ne 2981 . . . 4 (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
213166, 209resqrtcld 14276 . . . . . . 7 (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ)
214213recnd 10181 . . . . . 6 (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ)
21525, 193resqrtcld 14276 . . . . . . 7 (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ)
216215recnd 10181 . . . . . 6 (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ)
217214, 216sqmuld 13135 . . . . 5 (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)))
218167sqsqrtd 14298 . . . . . 6 (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋))
21926sqsqrtd 14298 . . . . . 6 (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌))
220218, 219oveq12d 6783 . . . . 5 (𝜑 → (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)) = ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
221217, 220eqtrd 2758 . . . 4 (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
222212, 171, 2213brtr4d 4792 . . 3 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2))
223213, 215remulcld 10183 . . . 4 (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ)
22418absge0d 14303 . . . 4 (𝜑 → 0 ≤ (abs‘(𝑋 , 𝑌)))
225166, 209sqrtge0d 14279 . . . . 5 (𝜑 → 0 ≤ (√‘(𝑋 , 𝑋)))
22625, 193sqrtge0d 14279 . . . . 5 (𝜑 → 0 ≤ (√‘(𝑌 , 𝑌)))
227213, 215, 225, 226mulge0d 10717 . . . 4 (𝜑 → 0 ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
228172, 223, 224, 227le2sqd 13159 . . 3 (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2)))
229222, 228mpbird 247 . 2 (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
230 lmodgrp 18993 . . . . 5 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
23143, 230syl 17 . . . 4 (𝜑𝑊 ∈ Grp)
232 ipcau2.n . . . . 5 𝑁 = (norm‘𝐺)
2334, 232, 5, 15tchnmval 23149 . . . 4 ((𝑊 ∈ Grp ∧ 𝑋𝑉) → (𝑁𝑋) = (√‘(𝑋 , 𝑋)))
234231, 13, 233syl2anc 696 . . 3 (𝜑 → (𝑁𝑋) = (√‘(𝑋 , 𝑋)))
2354, 232, 5, 15tchnmval 23149 . . . 4 ((𝑊 ∈ Grp ∧ 𝑌𝑉) → (𝑁𝑌) = (√‘(𝑌 , 𝑌)))
236231, 14, 235syl2anc 696 . . 3 (𝜑 → (𝑁𝑌) = (√‘(𝑌 , 𝑌)))
237234, 236oveq12d 6783 . 2 (𝜑 → ((𝑁𝑋) · (𝑁𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
238229, 237breqtrrd 4788 1 (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁𝑋) · (𝑁𝑌)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  wne 2896  wral 3014  Vcvv 3304  wss 3680   class class class wbr 4760  cfv 6001  (class class class)co 6765  cc 10047  cr 10048  0cc0 10049  1c1 10050   + caddc 10052   · cmul 10054   < clt 10187  cle 10188  cmin 10379   / cdiv 10797  2c2 11183  cexp 12975  ccj 13956  csqrt 14093  abscabs 14094  Basecbs 15980  s cress 15981  +gcplusg 16064  .rcmulr 16065  *𝑟cstv 16066  Scalarcsca 16067   ·𝑠 cvsca 16068  ·𝑖cip 16069  0gc0g 16223  Grpcgrp 17544  -gcsg 17546  DivRingcdr 18870  LModclmod 18986  LVecclvec 19225  fldccnfld 19869  PreHilcphl 20092  normcnm 22503  ℂModcclm 22983  toℂHilctch 23088
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127  ax-addf 10128  ax-mulf 10129
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-tpos 7472  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-1o 7680  df-oadd 7684  df-er 7862  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-fin 8076  df-sup 8464  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-3 11193  df-4 11194  df-5 11195  df-6 11196  df-7 11197  df-8 11198  df-9 11199  df-n0 11406  df-z 11491  df-dec 11607  df-uz 11801  df-rp 11947  df-fz 12441  df-seq 12917  df-exp 12976  df-cj 13959  df-re 13960  df-im 13961  df-sqrt 14095  df-abs 14096  df-struct 15982  df-ndx 15983  df-slot 15984  df-base 15986  df-sets 15987  df-ress 15988  df-plusg 16077  df-mulr 16078  df-starv 16079  df-sca 16080  df-vsca 16081  df-ip 16082  df-tset 16083  df-ple 16084  df-ds 16087  df-unif 16088  df-0g 16225  df-mgm 17364  df-sgrp 17406  df-mnd 17417  df-mhm 17457  df-grp 17547  df-minusg 17548  df-sbg 17549  df-subg 17713  df-ghm 17780  df-cmn 18316  df-abl 18317  df-mgp 18611  df-ur 18623  df-ring 18670  df-cring 18671  df-oppr 18744  df-dvdsr 18762  df-unit 18763  df-invr 18793  df-dvr 18804  df-rnghom 18838  df-drng 18872  df-subrg 18901  df-staf 18968  df-srng 18969  df-lmod 18988  df-lmhm 19145  df-lvec 19226  df-sra 19295  df-rgmod 19296  df-cnfld 19870  df-phl 20094  df-nm 22509  df-tng 22511  df-clm 22984  df-tch 23090
This theorem is referenced by:  tchcphlem1  23155  ipcau  23158
  Copyright terms: Public domain W3C validator