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

Theorem ipcau2 23879
 Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.)
Hypotheses
Ref Expression
tcphval.n 𝐺 = (toℂPreHil‘𝑊)
tcphcph.v 𝑉 = (Base‘𝑊)
tcphcph.f 𝐹 = (Scalar‘𝑊)
tcphcph.1 (𝜑𝑊 ∈ PreHil)
tcphcph.2 (𝜑𝐹 = (ℂflds 𝐾))
tcphcph.h , = (·𝑖𝑊)
tcphcph.3 ((𝜑 ∧ (𝑥𝐾𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)
tcphcph.4 ((𝜑𝑥𝑉) → 0 ≤ (𝑥 , 𝑥))
tcphcph.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 7153 . . . . . . 7 (𝑌 = (0g𝑊) → (𝑋 , 𝑌) = (𝑋 , (0g𝑊)))
21oveq1d 7160 . . . . . 6 (𝑌 = (0g𝑊) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) = ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)))
32breq1d 5044 . . . . 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 (𝜑𝐹 = (ℂflds 𝐾))
94, 5, 6, 7, 8phclm 23877 . . . . . . . . . . . 12 (𝜑𝑊 ∈ ℂMod)
10 tcphcph.k . . . . . . . . . . . . 13 𝐾 = (Base‘𝐹)
116, 10clmsscn 23725 . . . . . . . . . . . 12 (𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ)
129, 11syl 17 . . . . . . . . . . 11 (𝜑𝐾 ⊆ ℂ)
13 ipcau2.3 . . . . . . . . . . . 12 (𝜑𝑋𝑉)
14 ipcau2.4 . . . . . . . . . . . 12 (𝜑𝑌𝑉)
15 tcphcph.h . . . . . . . . . . . . 13 , = (·𝑖𝑊)
166, 15, 5, 10ipcl 20344 . . . . . . . . . . . 12 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉) → (𝑋 , 𝑌) ∈ 𝐾)
177, 13, 14, 16syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (𝑋 , 𝑌) ∈ 𝐾)
1812, 17sseldd 3918 . . . . . . . . . 10 (𝜑 → (𝑋 , 𝑌) ∈ ℂ)
1918adantr 484 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑌) ∈ ℂ)
206, 15, 5, 10ipcl 20344 . . . . . . . . . . . 12 ((𝑊 ∈ PreHil ∧ 𝑌𝑉𝑋𝑉) → (𝑌 , 𝑋) ∈ 𝐾)
217, 14, 13, 20syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (𝑌 , 𝑋) ∈ 𝐾)
2212, 21sseldd 3918 . . . . . . . . . 10 (𝜑 → (𝑌 , 𝑋) ∈ ℂ)
2322adantr 484 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑋) ∈ ℂ)
244, 5, 6, 7, 8, 15tcphcphlem3 23878 . . . . . . . . . . . 12 ((𝜑𝑌𝑉) → (𝑌 , 𝑌) ∈ ℝ)
2514, 24mpdan 686 . . . . . . . . . . 11 (𝜑 → (𝑌 , 𝑌) ∈ ℝ)
2625recnd 10676 . . . . . . . . . 10 (𝜑 → (𝑌 , 𝑌) ∈ ℂ)
2726adantr 484 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ ℂ)
286clm0 23718 . . . . . . . . . . . . . 14 (𝑊 ∈ ℂMod → 0 = (0g𝐹))
299, 28syl 17 . . . . . . . . . . . . 13 (𝜑 → 0 = (0g𝐹))
3029eqeq2d 2809 . . . . . . . . . . . 12 (𝜑 → ((𝑌 , 𝑌) = 0 ↔ (𝑌 , 𝑌) = (0g𝐹)))
31 eqid 2798 . . . . . . . . . . . . . 14 (0g𝐹) = (0g𝐹)
32 eqid 2798 . . . . . . . . . . . . . 14 (0g𝑊) = (0g𝑊)
336, 15, 5, 31, 32ipeq0 20349 . . . . . . . . . . . . 13 ((𝑊 ∈ PreHil ∧ 𝑌𝑉) → ((𝑌 , 𝑌) = (0g𝐹) ↔ 𝑌 = (0g𝑊)))
347, 14, 33syl2anc 587 . . . . . . . . . . . 12 (𝜑 → ((𝑌 , 𝑌) = (0g𝐹) ↔ 𝑌 = (0g𝑊)))
3530, 34bitrd 282 . . . . . . . . . . 11 (𝜑 → ((𝑌 , 𝑌) = 0 ↔ 𝑌 = (0g𝑊)))
3635necon3bid 3031 . . . . . . . . . 10 (𝜑 → ((𝑌 , 𝑌) ≠ 0 ↔ 𝑌 ≠ (0g𝑊)))
3736biimpar 481 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ≠ 0)
3819, 23, 27, 37divassd 11458 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))))
39 ipcau2.c . . . . . . . . 9 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌))
4039oveq2i 7156 . . . . . . . 8 ((𝑋 , 𝑌) · 𝐶) = ((𝑋 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))
4138, 40eqtr4di 2851 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · 𝐶))
42 oveq12 7154 . . . . . . . . . . . 12 ((𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∧ 𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) → (𝑥 , 𝑥) = ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
4342anidms 570 . . . . . . . . . . 11 (𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) → (𝑥 , 𝑥) = ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
4443breq2d 5046 . . . . . . . . . 10 (𝑥 = (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)))))
45 tcphcph.4 . . . . . . . . . . . 12 ((𝜑𝑥𝑉) → 0 ≤ (𝑥 , 𝑥))
4645ralrimiva 3149 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑉 0 ≤ (𝑥 , 𝑥))
4746adantr 484 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → ∀𝑥𝑉 0 ≤ (𝑥 , 𝑥))
48 phllmod 20341 . . . . . . . . . . . . 13 (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
497, 48syl 17 . . . . . . . . . . . 12 (𝜑𝑊 ∈ LMod)
5049adantr 484 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ LMod)
5113adantr 484 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑋𝑉)
5239fveq2i 6658 . . . . . . . . . . . . . . 15 (∗‘𝐶) = (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌)))
5323, 27, 37cjdivd 14594 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘((𝑌 , 𝑋) / (𝑌 , 𝑌))) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))))
5452, 53syl5eq 2845 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))))
558fveq2d 6659 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (*𝑟𝐹) = (*𝑟‘(ℂflds 𝐾)))
5610fvexi 6669 . . . . . . . . . . . . . . . . . . . . . 22 𝐾 ∈ V
57 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂflds 𝐾) = (ℂflds 𝐾)
58 cnfldcj 20119 . . . . . . . . . . . . . . . . . . . . . . 23 ∗ = (*𝑟‘ℂfld)
5957, 58ressstarv 16638 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 ∈ V → ∗ = (*𝑟‘(ℂflds 𝐾)))
6056, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 ∗ = (*𝑟‘(ℂflds 𝐾))
6155, 60eqtr4di 2851 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (*𝑟𝐹) = ∗)
6261fveq1d 6657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (∗‘(𝑋 , 𝑌)))
63 eqid 2798 . . . . . . . . . . . . . . . . . . . . 21 (*𝑟𝐹) = (*𝑟𝐹)
646, 15, 5, 63ipcj 20345 . . . . . . . . . . . . . . . . . . . 20 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉) → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
657, 13, 14, 64syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((*𝑟𝐹)‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6662, 65eqtr3d 2835 . . . . . . . . . . . . . . . . . 18 (𝜑 → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6766adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑋 , 𝑌)) = (𝑌 , 𝑋))
6867fveq2d 6659 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(∗‘(𝑋 , 𝑌))) = (∗‘(𝑌 , 𝑋)))
6919cjcjd 14570 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(∗‘(𝑋 , 𝑌))) = (𝑋 , 𝑌))
7068, 69eqtr3d 2835 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑌 , 𝑋)) = (𝑋 , 𝑌))
7125adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ ℝ)
7271cjred 14597 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘(𝑌 , 𝑌)) = (𝑌 , 𝑌))
7370, 72oveq12d 7163 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘(𝑌 , 𝑋)) / (∗‘(𝑌 , 𝑌))) = ((𝑋 , 𝑌) / (𝑌 , 𝑌)))
7419, 27, 37divrecd 11426 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) / (𝑌 , 𝑌)) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))))
7554, 73, 743eqtrd 2837 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))))
769adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ ℂMod)
7717adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑌) ∈ 𝐾)
786, 15, 5, 10ipcl 20344 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ PreHil ∧ 𝑌𝑉𝑌𝑉) → (𝑌 , 𝑌) ∈ 𝐾)
797, 14, 14, 78syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 , 𝑌) ∈ 𝐾)
8079adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑌) ∈ 𝐾)
818adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐹 = (ℂflds 𝐾))
82 phllvec 20340 . . . . . . . . . . . . . . . . . . 19 (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
837, 82syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ LVec)
846lvecdrng 19891 . . . . . . . . . . . . . . . . . 18 (𝑊 ∈ LVec → 𝐹 ∈ DivRing)
8583, 84syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ DivRing)
8685adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐹 ∈ DivRing)
8710, 81, 86cphreccllem 23824 . . . . . . . . . . . . . . 15 (((𝜑𝑌 ≠ (0g𝑊)) ∧ (𝑌 , 𝑌) ∈ 𝐾 ∧ (𝑌 , 𝑌) ≠ 0) → (1 / (𝑌 , 𝑌)) ∈ 𝐾)
8880, 37, 87mpd3an23 1460 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (1 / (𝑌 , 𝑌)) ∈ 𝐾)
896, 10clmmcl 23731 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
9076, 77, 88, 89syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
9175, 90eqeltrd 2890 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) ∈ 𝐾)
9214adantr 484 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑌𝑉)
93 eqid 2798 . . . . . . . . . . . . 13 ( ·𝑠𝑊) = ( ·𝑠𝑊)
945, 6, 93, 10lmodvscl 19665 . . . . . . . . . . . 12 ((𝑊 ∈ LMod ∧ (∗‘𝐶) ∈ 𝐾𝑌𝑉) → ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)
9550, 91, 92, 94syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)
96 eqid 2798 . . . . . . . . . . . 12 (-g𝑊) = (-g𝑊)
975, 96lmodvsubcl 19693 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ 𝑋𝑉 ∧ ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉) → (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∈ 𝑉)
9850, 51, 95, 97syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) ∈ 𝑉)
9944, 47, 98rspcdva 3574 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))))
100 eqid 2798 . . . . . . . . . . 11 (-g𝐹) = (-g𝐹)
101 eqid 2798 . . . . . . . . . . 11 (+g𝐹) = (+g𝐹)
1027adantr 484 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → 𝑊 ∈ PreHil)
1036, 15, 5, 96, 100, 101, 102, 51, 95, 51, 95ip2subdi 20355 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) = (((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))(-g𝐹)((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋))))
10481fveq2d 6659 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (+g𝐹) = (+g‘(ℂflds 𝐾)))
105 cnfldadd 20117 . . . . . . . . . . . . . . 15 + = (+g‘ℂfld)
10657, 105ressplusg 16624 . . . . . . . . . . . . . 14 (𝐾 ∈ V → + = (+g‘(ℂflds 𝐾)))
10756, 106ax-mp 5 . . . . . . . . . . . . 13 + = (+g‘(ℂflds 𝐾))
108104, 107eqtr4di 2851 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (+g𝐹) = + )
109 eqidd 2799 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) = (𝑋 , 𝑋))
110 eqid 2798 . . . . . . . . . . . . . . 15 (.r𝐹) = (.r𝐹)
1116, 15, 5, 10, 93, 110ipass 20356 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ ((∗‘𝐶) ∈ 𝐾𝑌𝑉 ∧ ((∗‘𝐶)( ·𝑠𝑊)𝑌) ∈ 𝑉)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))))
112102, 91, 92, 95, 111syl13anc 1369 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))))
11381fveq2d 6659 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (.r𝐹) = (.r‘(ℂflds 𝐾)))
114 cnfldmul 20118 . . . . . . . . . . . . . . . . 17 · = (.r‘ℂfld)
11557, 114ressmulr 16637 . . . . . . . . . . . . . . . 16 (𝐾 ∈ V → · = (.r‘(ℂflds 𝐾)))
11656, 115ax-mp 5 . . . . . . . . . . . . . . 15 · = (.r‘(ℂflds 𝐾))
117113, 116eqtr4di 2851 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (.r𝐹) = · )
118 eqidd 2799 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (∗‘𝐶) = (∗‘𝐶))
11923, 27, 37divrecd 11426 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑋) / (𝑌 , 𝑌)) = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))))
12039, 119syl5eq 2845 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐶 = ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))))
12121adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , 𝑋) ∈ 𝐾)
1226, 10clmmcl 23731 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ ℂMod ∧ (𝑌 , 𝑋) ∈ 𝐾 ∧ (1 / (𝑌 , 𝑌)) ∈ 𝐾) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
12376, 121, 88, 122syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑋) · (1 / (𝑌 , 𝑌))) ∈ 𝐾)
124120, 123eqeltrd 2890 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐶𝐾)
1256, 15, 5, 10, 93, 110, 63ipassr2 20358 . . . . . . . . . . . . . . . 16 ((𝑊 ∈ PreHil ∧ (𝑌𝑉𝑌𝑉𝐶𝐾)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
126102, 92, 92, 124, 125syl13anc 1369 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
127117oveqd 7162 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = ((𝑌 , 𝑌) · 𝐶))
12839oveq2i 7156 . . . . . . . . . . . . . . . . 17 ((𝑌 , 𝑌) · 𝐶) = ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌)))
12923, 27, 37divcan2d 11425 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌) · ((𝑌 , 𝑋) / (𝑌 , 𝑌))) = (𝑌 , 𝑋))
130128, 129syl5eq 2845 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌) · 𝐶) = (𝑌 , 𝑋))
131127, 130eqtrd 2833 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑌 , 𝑌)(.r𝐹)𝐶) = (𝑌 , 𝑋))
13261adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑌 ≠ (0g𝑊)) → (*𝑟𝐹) = ∗)
133132fveq1d 6657 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≠ (0g𝑊)) → ((*𝑟𝐹)‘𝐶) = (∗‘𝐶))
134133oveq1d 7160 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≠ (0g𝑊)) → (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌) = ((∗‘𝐶)( ·𝑠𝑊)𝑌))
135134oveq2d 7161 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))
136126, 131, 1353eqtr3rd 2842 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑌 , 𝑋))
137117, 118, 136oveq123d 7166 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)(.r𝐹)(𝑌 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((∗‘𝐶) · (𝑌 , 𝑋)))
138112, 137eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((∗‘𝐶) · (𝑌 , 𝑋)))
139108, 109, 138oveq123d 7166 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))))
1406, 15, 5, 10, 93, 110, 63ipassr2 20358 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ (𝑋𝑉𝑌𝑉𝐶𝐾)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
141102, 51, 92, 124, 140syl13anc 1369 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)))
142117oveqd 7162 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌)(.r𝐹)𝐶) = ((𝑋 , 𝑌) · 𝐶))
143134oveq2d 7161 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , (((*𝑟𝐹)‘𝐶)( ·𝑠𝑊)𝑌)) = (𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))
144141, 142, 1433eqtr3rd 2842 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌)) = ((𝑋 , 𝑌) · 𝐶))
1456, 15, 5, 10, 93, 110ipass 20356 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ ((∗‘𝐶) ∈ 𝐾𝑌𝑉𝑋𝑉)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)))
146102, 91, 92, 51, 145syl13anc 1369 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)))
147117oveqd 7162 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶)(.r𝐹)(𝑌 , 𝑋)) = ((∗‘𝐶) · (𝑌 , 𝑋)))
148146, 147eqtrd 2833 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋) = ((∗‘𝐶) · (𝑌 , 𝑋)))
149108, 144, 148oveq123d 7166 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋)) = (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))))
150139, 149oveq12d 7163 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋)(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , ((∗‘𝐶)( ·𝑠𝑊)𝑌)))(-g𝐹)((𝑋 , ((∗‘𝐶)( ·𝑠𝑊)𝑌))(+g𝐹)(((∗‘𝐶)( ·𝑠𝑊)𝑌) , 𝑋))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
1516, 15, 5, 10ipcl 20344 . . . . . . . . . . . . . 14 ((𝑊 ∈ PreHil ∧ 𝑋𝑉𝑋𝑉) → (𝑋 , 𝑋) ∈ 𝐾)
152102, 51, 51, 151syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ 𝐾)
1536, 10clmmcl 23731 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (∗‘𝐶) ∈ 𝐾 ∧ (𝑌 , 𝑋) ∈ 𝐾) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾)
15476, 91, 121, 153syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾)
1556, 10clmacl 23730 . . . . . . . . . . . . 13 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑋) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
15676, 152, 154, 155syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
1576, 10clmmcl 23731 . . . . . . . . . . . . . 14 ((𝑊 ∈ ℂMod ∧ (𝑋 , 𝑌) ∈ 𝐾𝐶𝐾) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾)
15876, 77, 124, 157syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾)
1596, 10clmacl 23730 . . . . . . . . . . . . 13 ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑌) · 𝐶) ∈ 𝐾 ∧ ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ 𝐾) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
16076, 158, 154, 159syl3anc 1368 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾)
1616, 10clmsub 23726 . . . . . . . . . . . 12 ((𝑊 ∈ ℂMod ∧ ((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾 ∧ (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋))) ∈ 𝐾) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
16276, 156, 160, 161syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))))
1634, 5, 6, 7, 8, 15tcphcphlem3 23878 . . . . . . . . . . . . . . 15 ((𝜑𝑋𝑉) → (𝑋 , 𝑋) ∈ ℝ)
16413, 163mpdan 686 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 , 𝑋) ∈ ℝ)
165164recnd 10676 . . . . . . . . . . . . 13 (𝜑 → (𝑋 , 𝑋) ∈ ℂ)
166165adantr 484 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ ℂ)
16718absvalsqd 14814 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))))
16866oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑋 , 𝑌) · (∗‘(𝑋 , 𝑌))) = ((𝑋 , 𝑌) · (𝑌 , 𝑋)))
169167, 168eqtrd 2833 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) = ((𝑋 , 𝑌) · (𝑌 , 𝑋)))
17018abscld 14808 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘(𝑋 , 𝑌)) ∈ ℝ)
171170resqcld 13627 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ∈ ℝ)
172169, 171eqeltrrd 2891 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ)
173172adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ)
174173, 71, 37redivcld 11475 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ∈ ℝ)
17541, 174eqeltrrd 2891 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℝ)
176175recnd 10676 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ∈ ℂ)
17776, 11syl 17 . . . . . . . . . . . . 13 ((𝜑𝑌 ≠ (0g𝑊)) → 𝐾 ⊆ ℂ)
178177, 154sseldd 3918 . . . . . . . . . . . 12 ((𝜑𝑌 ≠ (0g𝑊)) → ((∗‘𝐶) · (𝑌 , 𝑋)) ∈ ℂ)
179166, 176, 178pnpcan2d 11042 . . . . . . . . . . 11 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋))) − (((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
180162, 179eqtr3d 2835 . . . . . . . . . 10 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑋) + ((∗‘𝐶) · (𝑌 , 𝑋)))(-g𝐹)(((𝑋 , 𝑌) · 𝐶) + ((∗‘𝐶) · (𝑌 , 𝑋)))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
181103, 150, 1803eqtrd 2837 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌)) , (𝑋(-g𝑊)((∗‘𝐶)( ·𝑠𝑊)𝑌))) = ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
18299, 181breqtrd 5060 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)))
183164adantr 484 . . . . . . . . 9 ((𝜑𝑌 ≠ (0g𝑊)) → (𝑋 , 𝑋) ∈ ℝ)
184183, 175subge0d 11237 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → (0 ≤ ((𝑋 , 𝑋) − ((𝑋 , 𝑌) · 𝐶)) ↔ ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋)))
185182, 184mpbid 235 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · 𝐶) ≤ (𝑋 , 𝑋))
18641, 185eqbrtrd 5056 . . . . . 6 ((𝜑𝑌 ≠ (0g𝑊)) → (((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋))
187 oveq12 7154 . . . . . . . . . . . 12 ((𝑥 = 𝑌𝑥 = 𝑌) → (𝑥 , 𝑥) = (𝑌 , 𝑌))
188187anidms 570 . . . . . . . . . . 11 (𝑥 = 𝑌 → (𝑥 , 𝑥) = (𝑌 , 𝑌))
189188breq2d 5046 . . . . . . . . . 10 (𝑥 = 𝑌 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑌 , 𝑌)))
190189, 46, 14rspcdva 3574 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑌 , 𝑌))
191190adantr 484 . . . . . . . 8 ((𝜑𝑌 ≠ (0g𝑊)) → 0 ≤ (𝑌 , 𝑌))
19271, 191, 37ne0gt0d 10784 . . . . . . 7 ((𝜑𝑌 ≠ (0g𝑊)) → 0 < (𝑌 , 𝑌))
193 ledivmul2 11526 . . . . . . 7 ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) ∈ ℝ ∧ (𝑋 , 𝑋) ∈ ℝ ∧ ((𝑌 , 𝑌) ∈ ℝ ∧ 0 < (𝑌 , 𝑌))) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))))
194173, 183, 71, 192, 193syl112anc 1371 . . . . . 6 ((𝜑𝑌 ≠ (0g𝑊)) → ((((𝑋 , 𝑌) · (𝑌 , 𝑋)) / (𝑌 , 𝑌)) ≤ (𝑋 , 𝑋) ↔ ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌))))
195186, 194mpbid 235 . . . . 5 ((𝜑𝑌 ≠ (0g𝑊)) → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
1966, 15, 5, 31, 32ip0r 20348 . . . . . . . . . 10 ((𝑊 ∈ PreHil ∧ 𝑋𝑉) → (𝑋 , (0g𝑊)) = (0g𝐹))
1977, 13, 196syl2anc 587 . . . . . . . . 9 (𝜑 → (𝑋 , (0g𝑊)) = (0g𝐹))
198197, 29eqtr4d 2836 . . . . . . . 8 (𝜑 → (𝑋 , (0g𝑊)) = 0)
199198oveq1d 7160 . . . . . . 7 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) = (0 · (𝑌 , 𝑋)))
20022mul02d 10845 . . . . . . 7 (𝜑 → (0 · (𝑌 , 𝑋)) = 0)
201199, 200eqtrd 2833 . . . . . 6 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) = 0)
202 oveq12 7154 . . . . . . . . . 10 ((𝑥 = 𝑋𝑥 = 𝑋) → (𝑥 , 𝑥) = (𝑋 , 𝑋))
203202anidms 570 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥 , 𝑥) = (𝑋 , 𝑋))
204203breq2d 5046 . . . . . . . 8 (𝑥 = 𝑋 → (0 ≤ (𝑥 , 𝑥) ↔ 0 ≤ (𝑋 , 𝑋)))
205204, 46, 13rspcdva 3574 . . . . . . 7 (𝜑 → 0 ≤ (𝑋 , 𝑋))
206164, 25, 205, 190mulge0d 11224 . . . . . 6 (𝜑 → 0 ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
207201, 206eqbrtrd 5056 . . . . 5 (𝜑 → ((𝑋 , (0g𝑊)) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
2083, 195, 207pm2.61ne 3072 . . . 4 (𝜑 → ((𝑋 , 𝑌) · (𝑌 , 𝑋)) ≤ ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
209164, 205resqrtcld 14789 . . . . . . 7 (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℝ)
210209recnd 10676 . . . . . 6 (𝜑 → (√‘(𝑋 , 𝑋)) ∈ ℂ)
21125, 190resqrtcld 14789 . . . . . . 7 (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℝ)
212211recnd 10676 . . . . . 6 (𝜑 → (√‘(𝑌 , 𝑌)) ∈ ℂ)
213210, 212sqmuld 13538 . . . . 5 (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)))
214165sqsqrtd 14811 . . . . . 6 (𝜑 → ((√‘(𝑋 , 𝑋))↑2) = (𝑋 , 𝑋))
21526sqsqrtd 14811 . . . . . 6 (𝜑 → ((√‘(𝑌 , 𝑌))↑2) = (𝑌 , 𝑌))
216214, 215oveq12d 7163 . . . . 5 (𝜑 → (((√‘(𝑋 , 𝑋))↑2) · ((√‘(𝑌 , 𝑌))↑2)) = ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
217213, 216eqtrd 2833 . . . 4 (𝜑 → (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2) = ((𝑋 , 𝑋) · (𝑌 , 𝑌)))
218208, 169, 2173brtr4d 5066 . . 3 (𝜑 → ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2))
219209, 211remulcld 10678 . . . 4 (𝜑 → ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ∈ ℝ)
22018absge0d 14816 . . . 4 (𝜑 → 0 ≤ (abs‘(𝑋 , 𝑌)))
221164, 205sqrtge0d 14792 . . . . 5 (𝜑 → 0 ≤ (√‘(𝑋 , 𝑋)))
22225, 190sqrtge0d 14792 . . . . 5 (𝜑 → 0 ≤ (√‘(𝑌 , 𝑌)))
223209, 211, 221, 222mulge0d 11224 . . . 4 (𝜑 → 0 ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
224170, 219, 220, 223le2sqd 13636 . . 3 (𝜑 → ((abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))) ↔ ((abs‘(𝑋 , 𝑌))↑2) ≤ (((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌)))↑2)))
225218, 224mpbird 260 . 2 (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
226 lmodgrp 19655 . . . . 5 (𝑊 ∈ LMod → 𝑊 ∈ Grp)
22749, 226syl 17 . . . 4 (𝜑𝑊 ∈ Grp)
228 ipcau2.n . . . . 5 𝑁 = (norm‘𝐺)
2294, 228, 5, 15tcphnmval 23874 . . . 4 ((𝑊 ∈ Grp ∧ 𝑋𝑉) → (𝑁𝑋) = (√‘(𝑋 , 𝑋)))
230227, 13, 229syl2anc 587 . . 3 (𝜑 → (𝑁𝑋) = (√‘(𝑋 , 𝑋)))
2314, 228, 5, 15tcphnmval 23874 . . . 4 ((𝑊 ∈ Grp ∧ 𝑌𝑉) → (𝑁𝑌) = (√‘(𝑌 , 𝑌)))
232227, 14, 231syl2anc 587 . . 3 (𝜑 → (𝑁𝑌) = (√‘(𝑌 , 𝑌)))
233230, 232oveq12d 7163 . 2 (𝜑 → ((𝑁𝑋) · (𝑁𝑌)) = ((√‘(𝑋 , 𝑋)) · (√‘(𝑌 , 𝑌))))
234225, 233breqtrrd 5062 1 (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁𝑋) · (𝑁𝑌)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  Vcvv 3442   ⊆ wss 3883   class class class wbr 5034  ‘cfv 6332  (class class class)co 7145  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545   + caddc 10547   · cmul 10549   < clt 10682   ≤ cle 10683   − cmin 10877   / cdiv 11304  2c2 11698  ↑cexp 13445  ∗ccj 14467  √csqrt 14604  abscabs 14605  Basecbs 16495   ↾s cress 16496  +gcplusg 16577  .rcmulr 16578  *𝑟cstv 16579  Scalarcsca 16580   ·𝑠 cvsca 16581  ·𝑖cip 16582  0gc0g 16725  Grpcgrp 18115  -gcsg 18117  DivRingcdr 19516  LModclmod 19648  LVecclvec 19888  ℂfldccnfld 20112  PreHilcphl 20335  normcnm 23224  ℂModcclm 23708  toℂPreHilctcph 23813 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622  ax-addf 10623  ax-mulf 10624 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-tpos 7893  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-oadd 8107  df-er 8290  df-map 8409  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-sup 8908  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-z 11990  df-dec 12107  df-uz 12252  df-rp 12398  df-fz 12906  df-seq 13385  df-exp 13446  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-mulr 16591  df-starv 16592  df-sca 16593  df-vsca 16594  df-ip 16595  df-tset 16596  df-ple 16597  df-ds 16599  df-unif 16600  df-0g 16727  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-mhm 17968  df-grp 18118  df-minusg 18119  df-sbg 18120  df-subg 18289  df-ghm 18369  df-cmn 18921  df-abl 18922  df-mgp 19254  df-ur 19266  df-ring 19313  df-cring 19314  df-oppr 19390  df-dvdsr 19408  df-unit 19409  df-invr 19439  df-dvr 19450  df-rnghom 19484  df-drng 19518  df-subrg 19547  df-staf 19630  df-srng 19631  df-lmod 19650  df-lmhm 19808  df-lvec 19889  df-sra 19958  df-rgmod 19959  df-cnfld 20113  df-phl 20337  df-nm 23230  df-tng 23232  df-clm 23709  df-tcph 23815 This theorem is referenced by:  tcphcphlem1  23880  ipcau  23883
 Copyright terms: Public domain W3C validator