Metamath Proof Explorer


Theorem ipcau2

Description: The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau . (Contributed by Mario Carneiro, 11-Oct-2015)

Ref Expression
Hypotheses 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 ipcau2 ( 𝜑 → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphcph.v 𝑉 = ( Base ‘ 𝑊 )
3 tcphcph.f 𝐹 = ( Scalar ‘ 𝑊 )
4 tcphcph.1 ( 𝜑𝑊 ∈ PreHil )
5 tcphcph.2 ( 𝜑𝐹 = ( ℂflds 𝐾 ) )
6 tcphcph.h , = ( ·𝑖𝑊 )
7 tcphcph.3 ( ( 𝜑 ∧ ( 𝑥𝐾𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( √ ‘ 𝑥 ) ∈ 𝐾 )
8 tcphcph.4 ( ( 𝜑𝑥𝑉 ) → 0 ≤ ( 𝑥 , 𝑥 ) )
9 tcphcph.k 𝐾 = ( Base ‘ 𝐹 )
10 ipcau2.n 𝑁 = ( norm ‘ 𝐺 )
11 ipcau2.c 𝐶 = ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) )
12 ipcau2.3 ( 𝜑𝑋𝑉 )
13 ipcau2.4 ( 𝜑𝑌𝑉 )
14 oveq2 ( 𝑌 = ( 0g𝑊 ) → ( 𝑋 , 𝑌 ) = ( 𝑋 , ( 0g𝑊 ) ) )
15 14 oveq1d ( 𝑌 = ( 0g𝑊 ) → ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) = ( ( 𝑋 , ( 0g𝑊 ) ) · ( 𝑌 , 𝑋 ) ) )
16 15 breq1d ( 𝑌 = ( 0g𝑊 ) → ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) ↔ ( ( 𝑋 , ( 0g𝑊 ) ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) ) )
17 1 2 3 4 5 phclm ( 𝜑𝑊 ∈ ℂMod )
18 3 9 clmsscn ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
19 17 18 syl ( 𝜑𝐾 ⊆ ℂ )
20 3 6 2 9 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 , 𝑌 ) ∈ 𝐾 )
21 4 12 13 20 syl3anc ( 𝜑 → ( 𝑋 , 𝑌 ) ∈ 𝐾 )
22 19 21 sseldd ( 𝜑 → ( 𝑋 , 𝑌 ) ∈ ℂ )
23 22 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑌 ) ∈ ℂ )
24 3 6 2 9 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝑌𝑉𝑋𝑉 ) → ( 𝑌 , 𝑋 ) ∈ 𝐾 )
25 4 13 12 24 syl3anc ( 𝜑 → ( 𝑌 , 𝑋 ) ∈ 𝐾 )
26 19 25 sseldd ( 𝜑 → ( 𝑌 , 𝑋 ) ∈ ℂ )
27 26 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑋 ) ∈ ℂ )
28 1 2 3 4 5 6 tcphcphlem3 ( ( 𝜑𝑌𝑉 ) → ( 𝑌 , 𝑌 ) ∈ ℝ )
29 13 28 mpdan ( 𝜑 → ( 𝑌 , 𝑌 ) ∈ ℝ )
30 29 recnd ( 𝜑 → ( 𝑌 , 𝑌 ) ∈ ℂ )
31 30 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑌 ) ∈ ℂ )
32 3 clm0 ( 𝑊 ∈ ℂMod → 0 = ( 0g𝐹 ) )
33 17 32 syl ( 𝜑 → 0 = ( 0g𝐹 ) )
34 33 eqeq2d ( 𝜑 → ( ( 𝑌 , 𝑌 ) = 0 ↔ ( 𝑌 , 𝑌 ) = ( 0g𝐹 ) ) )
35 eqid ( 0g𝐹 ) = ( 0g𝐹 )
36 eqid ( 0g𝑊 ) = ( 0g𝑊 )
37 3 6 2 35 36 ipeq0 ( ( 𝑊 ∈ PreHil ∧ 𝑌𝑉 ) → ( ( 𝑌 , 𝑌 ) = ( 0g𝐹 ) ↔ 𝑌 = ( 0g𝑊 ) ) )
38 4 13 37 syl2anc ( 𝜑 → ( ( 𝑌 , 𝑌 ) = ( 0g𝐹 ) ↔ 𝑌 = ( 0g𝑊 ) ) )
39 34 38 bitrd ( 𝜑 → ( ( 𝑌 , 𝑌 ) = 0 ↔ 𝑌 = ( 0g𝑊 ) ) )
40 39 necon3bid ( 𝜑 → ( ( 𝑌 , 𝑌 ) ≠ 0 ↔ 𝑌 ≠ ( 0g𝑊 ) ) )
41 40 biimpar ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑌 ) ≠ 0 )
42 23 27 31 41 divassd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) = ( ( 𝑋 , 𝑌 ) · ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) ) )
43 11 oveq2i ( ( 𝑋 , 𝑌 ) · 𝐶 ) = ( ( 𝑋 , 𝑌 ) · ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) )
44 42 43 eqtr4di ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) = ( ( 𝑋 , 𝑌 ) · 𝐶 ) )
45 oveq12 ( ( 𝑥 = ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ∧ 𝑥 = ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) → ( 𝑥 , 𝑥 ) = ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) )
46 45 anidms ( 𝑥 = ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) → ( 𝑥 , 𝑥 ) = ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) )
47 46 breq2d ( 𝑥 = ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) → ( 0 ≤ ( 𝑥 , 𝑥 ) ↔ 0 ≤ ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) ) )
48 8 ralrimiva ( 𝜑 → ∀ 𝑥𝑉 0 ≤ ( 𝑥 , 𝑥 ) )
49 48 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ∀ 𝑥𝑉 0 ≤ ( 𝑥 , 𝑥 ) )
50 phllmod ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
51 4 50 syl ( 𝜑𝑊 ∈ LMod )
52 51 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝑊 ∈ LMod )
53 12 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝑋𝑉 )
54 11 fveq2i ( ∗ ‘ 𝐶 ) = ( ∗ ‘ ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) )
55 27 31 41 cjdivd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) ) = ( ( ∗ ‘ ( 𝑌 , 𝑋 ) ) / ( ∗ ‘ ( 𝑌 , 𝑌 ) ) ) )
56 54 55 syl5eq ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ 𝐶 ) = ( ( ∗ ‘ ( 𝑌 , 𝑋 ) ) / ( ∗ ‘ ( 𝑌 , 𝑌 ) ) ) )
57 5 fveq2d ( 𝜑 → ( *𝑟𝐹 ) = ( *𝑟 ‘ ( ℂflds 𝐾 ) ) )
58 9 fvexi 𝐾 ∈ V
59 eqid ( ℂflds 𝐾 ) = ( ℂflds 𝐾 )
60 cnfldcj ∗ = ( *𝑟 ‘ ℂfld )
61 59 60 ressstarv ( 𝐾 ∈ V → ∗ = ( *𝑟 ‘ ( ℂflds 𝐾 ) ) )
62 58 61 ax-mp ∗ = ( *𝑟 ‘ ( ℂflds 𝐾 ) )
63 57 62 eqtr4di ( 𝜑 → ( *𝑟𝐹 ) = ∗ )
64 63 fveq1d ( 𝜑 → ( ( *𝑟𝐹 ) ‘ ( 𝑋 , 𝑌 ) ) = ( ∗ ‘ ( 𝑋 , 𝑌 ) ) )
65 eqid ( *𝑟𝐹 ) = ( *𝑟𝐹 )
66 3 6 2 65 ipcj ( ( 𝑊 ∈ PreHil ∧ 𝑋𝑉𝑌𝑉 ) → ( ( *𝑟𝐹 ) ‘ ( 𝑋 , 𝑌 ) ) = ( 𝑌 , 𝑋 ) )
67 4 12 13 66 syl3anc ( 𝜑 → ( ( *𝑟𝐹 ) ‘ ( 𝑋 , 𝑌 ) ) = ( 𝑌 , 𝑋 ) )
68 64 67 eqtr3d ( 𝜑 → ( ∗ ‘ ( 𝑋 , 𝑌 ) ) = ( 𝑌 , 𝑋 ) )
69 68 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( 𝑋 , 𝑌 ) ) = ( 𝑌 , 𝑋 ) )
70 69 fveq2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( ∗ ‘ ( 𝑋 , 𝑌 ) ) ) = ( ∗ ‘ ( 𝑌 , 𝑋 ) ) )
71 23 cjcjd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( ∗ ‘ ( 𝑋 , 𝑌 ) ) ) = ( 𝑋 , 𝑌 ) )
72 70 71 eqtr3d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( 𝑌 , 𝑋 ) ) = ( 𝑋 , 𝑌 ) )
73 29 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑌 ) ∈ ℝ )
74 73 cjred ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ ( 𝑌 , 𝑌 ) ) = ( 𝑌 , 𝑌 ) )
75 72 74 oveq12d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ ( 𝑌 , 𝑋 ) ) / ( ∗ ‘ ( 𝑌 , 𝑌 ) ) ) = ( ( 𝑋 , 𝑌 ) / ( 𝑌 , 𝑌 ) ) )
76 23 31 41 divrecd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) / ( 𝑌 , 𝑌 ) ) = ( ( 𝑋 , 𝑌 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) )
77 56 75 76 3eqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ 𝐶 ) = ( ( 𝑋 , 𝑌 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) )
78 17 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝑊 ∈ ℂMod )
79 21 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑌 ) ∈ 𝐾 )
80 3 6 2 9 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝑌𝑉𝑌𝑉 ) → ( 𝑌 , 𝑌 ) ∈ 𝐾 )
81 4 13 13 80 syl3anc ( 𝜑 → ( 𝑌 , 𝑌 ) ∈ 𝐾 )
82 81 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑌 ) ∈ 𝐾 )
83 5 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝐹 = ( ℂflds 𝐾 ) )
84 phllvec ( 𝑊 ∈ PreHil → 𝑊 ∈ LVec )
85 4 84 syl ( 𝜑𝑊 ∈ LVec )
86 3 lvecdrng ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
87 85 86 syl ( 𝜑𝐹 ∈ DivRing )
88 87 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝐹 ∈ DivRing )
89 9 83 88 cphreccllem ( ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) ∧ ( 𝑌 , 𝑌 ) ∈ 𝐾 ∧ ( 𝑌 , 𝑌 ) ≠ 0 ) → ( 1 / ( 𝑌 , 𝑌 ) ) ∈ 𝐾 )
90 82 41 89 mpd3an23 ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 1 / ( 𝑌 , 𝑌 ) ) ∈ 𝐾 )
91 3 9 clmmcl ( ( 𝑊 ∈ ℂMod ∧ ( 𝑋 , 𝑌 ) ∈ 𝐾 ∧ ( 1 / ( 𝑌 , 𝑌 ) ) ∈ 𝐾 ) → ( ( 𝑋 , 𝑌 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) ∈ 𝐾 )
92 78 79 90 91 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) ∈ 𝐾 )
93 77 92 eqeltrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ 𝐶 ) ∈ 𝐾 )
94 13 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝑌𝑉 )
95 eqid ( ·𝑠𝑊 ) = ( ·𝑠𝑊 )
96 2 3 95 9 lmodvscl ( ( 𝑊 ∈ LMod ∧ ( ∗ ‘ 𝐶 ) ∈ 𝐾𝑌𝑉 ) → ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ∈ 𝑉 )
97 52 93 94 96 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ∈ 𝑉 )
98 eqid ( -g𝑊 ) = ( -g𝑊 )
99 2 98 lmodvsubcl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ∧ ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ∈ 𝑉 ) → ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ∈ 𝑉 )
100 52 53 97 99 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ∈ 𝑉 )
101 47 49 100 rspcdva ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 0 ≤ ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) )
102 eqid ( -g𝐹 ) = ( -g𝐹 )
103 eqid ( +g𝐹 ) = ( +g𝐹 )
104 4 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝑊 ∈ PreHil )
105 3 6 2 98 102 103 104 53 97 53 97 ip2subdi ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) = ( ( ( 𝑋 , 𝑋 ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) ( -g𝐹 ) ( ( 𝑋 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) ) ) )
106 83 fveq2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( +g𝐹 ) = ( +g ‘ ( ℂflds 𝐾 ) ) )
107 cnfldadd + = ( +g ‘ ℂfld )
108 59 107 ressplusg ( 𝐾 ∈ V → + = ( +g ‘ ( ℂflds 𝐾 ) ) )
109 58 108 ax-mp + = ( +g ‘ ( ℂflds 𝐾 ) )
110 106 109 eqtr4di ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( +g𝐹 ) = + )
111 eqidd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑋 ) = ( 𝑋 , 𝑋 ) )
112 eqid ( .r𝐹 ) = ( .r𝐹 )
113 3 6 2 9 95 112 ipass ( ( 𝑊 ∈ PreHil ∧ ( ( ∗ ‘ 𝐶 ) ∈ 𝐾𝑌𝑉 ∧ ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ∈ 𝑉 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) )
114 104 93 94 97 113 syl13anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) )
115 83 fveq2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( .r𝐹 ) = ( .r ‘ ( ℂflds 𝐾 ) ) )
116 cnfldmul · = ( .r ‘ ℂfld )
117 59 116 ressmulr ( 𝐾 ∈ V → · = ( .r ‘ ( ℂflds 𝐾 ) ) )
118 58 117 ax-mp · = ( .r ‘ ( ℂflds 𝐾 ) )
119 115 118 eqtr4di ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( .r𝐹 ) = · )
120 eqidd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ∗ ‘ 𝐶 ) = ( ∗ ‘ 𝐶 ) )
121 27 31 41 divrecd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) = ( ( 𝑌 , 𝑋 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) )
122 11 121 syl5eq ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝐶 = ( ( 𝑌 , 𝑋 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) )
123 25 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , 𝑋 ) ∈ 𝐾 )
124 3 9 clmmcl ( ( 𝑊 ∈ ℂMod ∧ ( 𝑌 , 𝑋 ) ∈ 𝐾 ∧ ( 1 / ( 𝑌 , 𝑌 ) ) ∈ 𝐾 ) → ( ( 𝑌 , 𝑋 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) ∈ 𝐾 )
125 78 123 90 124 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑋 ) · ( 1 / ( 𝑌 , 𝑌 ) ) ) ∈ 𝐾 )
126 122 125 eqeltrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝐶𝐾 )
127 3 6 2 9 95 112 65 ipassr2 ( ( 𝑊 ∈ PreHil ∧ ( 𝑌𝑉𝑌𝑉𝐶𝐾 ) ) → ( ( 𝑌 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( 𝑌 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
128 104 94 94 126 127 syl13anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( 𝑌 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
129 119 oveqd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( ( 𝑌 , 𝑌 ) · 𝐶 ) )
130 11 oveq2i ( ( 𝑌 , 𝑌 ) · 𝐶 ) = ( ( 𝑌 , 𝑌 ) · ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) )
131 27 31 41 divcan2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑌 ) · ( ( 𝑌 , 𝑋 ) / ( 𝑌 , 𝑌 ) ) ) = ( 𝑌 , 𝑋 ) )
132 130 131 syl5eq ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑌 ) · 𝐶 ) = ( 𝑌 , 𝑋 ) )
133 129 132 eqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑌 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( 𝑌 , 𝑋 ) )
134 63 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( *𝑟𝐹 ) = ∗ )
135 134 fveq1d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( *𝑟𝐹 ) ‘ 𝐶 ) = ( ∗ ‘ 𝐶 ) )
136 135 oveq1d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) = ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) )
137 136 oveq2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( 𝑌 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
138 128 133 137 3eqtr3rd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑌 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( 𝑌 , 𝑋 ) )
139 119 120 138 oveq123d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) )
140 114 139 eqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) )
141 110 111 140 oveq123d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑋 ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) = ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) )
142 3 6 2 9 95 112 65 ipassr2 ( ( 𝑊 ∈ PreHil ∧ ( 𝑋𝑉𝑌𝑉𝐶𝐾 ) ) → ( ( 𝑋 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( 𝑋 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
143 104 53 94 126 142 syl13anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( 𝑋 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
144 119 oveqd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) ( .r𝐹 ) 𝐶 ) = ( ( 𝑋 , 𝑌 ) · 𝐶 ) )
145 136 oveq2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , ( ( ( *𝑟𝐹 ) ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( 𝑋 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) )
146 143 144 145 3eqtr3rd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) = ( ( 𝑋 , 𝑌 ) · 𝐶 ) )
147 3 6 2 9 95 112 ipass ( ( 𝑊 ∈ PreHil ∧ ( ( ∗ ‘ 𝐶 ) ∈ 𝐾𝑌𝑉𝑋𝑉 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) = ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , 𝑋 ) ) )
148 104 93 94 53 147 syl13anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) = ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , 𝑋 ) ) )
149 119 oveqd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ 𝐶 ) ( .r𝐹 ) ( 𝑌 , 𝑋 ) ) = ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) )
150 148 149 eqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) = ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) )
151 110 146 150 oveq123d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) ) = ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) )
152 141 151 oveq12d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑋 ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) ( -g𝐹 ) ( ( 𝑋 , ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ( +g𝐹 ) ( ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) , 𝑋 ) ) ) = ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ( -g𝐹 ) ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) )
153 3 6 2 9 ipcl ( ( 𝑊 ∈ PreHil ∧ 𝑋𝑉𝑋𝑉 ) → ( 𝑋 , 𝑋 ) ∈ 𝐾 )
154 104 53 53 153 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑋 ) ∈ 𝐾 )
155 3 9 clmmcl ( ( 𝑊 ∈ ℂMod ∧ ( ∗ ‘ 𝐶 ) ∈ 𝐾 ∧ ( 𝑌 , 𝑋 ) ∈ 𝐾 ) → ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ∈ 𝐾 )
156 78 93 123 155 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ∈ 𝐾 )
157 3 9 clmacl ( ( 𝑊 ∈ ℂMod ∧ ( 𝑋 , 𝑋 ) ∈ 𝐾 ∧ ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ∈ 𝐾 ) → ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 )
158 78 154 156 157 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 )
159 3 9 clmmcl ( ( 𝑊 ∈ ℂMod ∧ ( 𝑋 , 𝑌 ) ∈ 𝐾𝐶𝐾 ) → ( ( 𝑋 , 𝑌 ) · 𝐶 ) ∈ 𝐾 )
160 78 79 126 159 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · 𝐶 ) ∈ 𝐾 )
161 3 9 clmacl ( ( 𝑊 ∈ ℂMod ∧ ( ( 𝑋 , 𝑌 ) · 𝐶 ) ∈ 𝐾 ∧ ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ∈ 𝐾 ) → ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 )
162 78 160 156 161 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 )
163 3 9 clmsub ( ( 𝑊 ∈ ℂMod ∧ ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 ∧ ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ∈ 𝐾 ) → ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) − ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) = ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ( -g𝐹 ) ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) )
164 78 158 162 163 syl3anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) − ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) = ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ( -g𝐹 ) ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) )
165 1 2 3 4 5 6 tcphcphlem3 ( ( 𝜑𝑋𝑉 ) → ( 𝑋 , 𝑋 ) ∈ ℝ )
166 12 165 mpdan ( 𝜑 → ( 𝑋 , 𝑋 ) ∈ ℝ )
167 166 recnd ( 𝜑 → ( 𝑋 , 𝑋 ) ∈ ℂ )
168 167 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑋 ) ∈ ℂ )
169 22 absvalsqd ( 𝜑 → ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ↑ 2 ) = ( ( 𝑋 , 𝑌 ) · ( ∗ ‘ ( 𝑋 , 𝑌 ) ) ) )
170 68 oveq2d ( 𝜑 → ( ( 𝑋 , 𝑌 ) · ( ∗ ‘ ( 𝑋 , 𝑌 ) ) ) = ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) )
171 169 170 eqtrd ( 𝜑 → ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ↑ 2 ) = ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) )
172 22 abscld ( 𝜑 → ( abs ‘ ( 𝑋 , 𝑌 ) ) ∈ ℝ )
173 172 resqcld ( 𝜑 → ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ↑ 2 ) ∈ ℝ )
174 171 173 eqeltrrd ( 𝜑 → ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ∈ ℝ )
175 174 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ∈ ℝ )
176 175 73 41 redivcld ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) ∈ ℝ )
177 44 176 eqeltrrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · 𝐶 ) ∈ ℝ )
178 177 recnd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · 𝐶 ) ∈ ℂ )
179 78 18 syl ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 𝐾 ⊆ ℂ )
180 179 156 sseldd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ∈ ℂ )
181 168 178 180 pnpcan2d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) − ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) = ( ( 𝑋 , 𝑋 ) − ( ( 𝑋 , 𝑌 ) · 𝐶 ) ) )
182 164 181 eqtr3d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑋 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ( -g𝐹 ) ( ( ( 𝑋 , 𝑌 ) · 𝐶 ) + ( ( ∗ ‘ 𝐶 ) · ( 𝑌 , 𝑋 ) ) ) ) = ( ( 𝑋 , 𝑋 ) − ( ( 𝑋 , 𝑌 ) · 𝐶 ) ) )
183 105 152 182 3eqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) , ( 𝑋 ( -g𝑊 ) ( ( ∗ ‘ 𝐶 ) ( ·𝑠𝑊 ) 𝑌 ) ) ) = ( ( 𝑋 , 𝑋 ) − ( ( 𝑋 , 𝑌 ) · 𝐶 ) ) )
184 101 183 breqtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 0 ≤ ( ( 𝑋 , 𝑋 ) − ( ( 𝑋 , 𝑌 ) · 𝐶 ) ) )
185 166 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 𝑋 , 𝑋 ) ∈ ℝ )
186 185 177 subge0d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( 0 ≤ ( ( 𝑋 , 𝑋 ) − ( ( 𝑋 , 𝑌 ) · 𝐶 ) ) ↔ ( ( 𝑋 , 𝑌 ) · 𝐶 ) ≤ ( 𝑋 , 𝑋 ) ) )
187 184 186 mpbid ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · 𝐶 ) ≤ ( 𝑋 , 𝑋 ) )
188 44 187 eqbrtrd ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) ≤ ( 𝑋 , 𝑋 ) )
189 oveq12 ( ( 𝑥 = 𝑌𝑥 = 𝑌 ) → ( 𝑥 , 𝑥 ) = ( 𝑌 , 𝑌 ) )
190 189 anidms ( 𝑥 = 𝑌 → ( 𝑥 , 𝑥 ) = ( 𝑌 , 𝑌 ) )
191 190 breq2d ( 𝑥 = 𝑌 → ( 0 ≤ ( 𝑥 , 𝑥 ) ↔ 0 ≤ ( 𝑌 , 𝑌 ) ) )
192 191 48 13 rspcdva ( 𝜑 → 0 ≤ ( 𝑌 , 𝑌 ) )
193 192 adantr ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 0 ≤ ( 𝑌 , 𝑌 ) )
194 73 193 41 ne0gt0d ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → 0 < ( 𝑌 , 𝑌 ) )
195 ledivmul2 ( ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ∈ ℝ ∧ ( 𝑋 , 𝑋 ) ∈ ℝ ∧ ( ( 𝑌 , 𝑌 ) ∈ ℝ ∧ 0 < ( 𝑌 , 𝑌 ) ) ) → ( ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) ≤ ( 𝑋 , 𝑋 ) ↔ ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) ) )
196 175 185 73 194 195 syl112anc ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) / ( 𝑌 , 𝑌 ) ) ≤ ( 𝑋 , 𝑋 ) ↔ ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) ) )
197 188 196 mpbid ( ( 𝜑𝑌 ≠ ( 0g𝑊 ) ) → ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
198 3 6 2 35 36 ip0r ( ( 𝑊 ∈ PreHil ∧ 𝑋𝑉 ) → ( 𝑋 , ( 0g𝑊 ) ) = ( 0g𝐹 ) )
199 4 12 198 syl2anc ( 𝜑 → ( 𝑋 , ( 0g𝑊 ) ) = ( 0g𝐹 ) )
200 199 33 eqtr4d ( 𝜑 → ( 𝑋 , ( 0g𝑊 ) ) = 0 )
201 200 oveq1d ( 𝜑 → ( ( 𝑋 , ( 0g𝑊 ) ) · ( 𝑌 , 𝑋 ) ) = ( 0 · ( 𝑌 , 𝑋 ) ) )
202 26 mul02d ( 𝜑 → ( 0 · ( 𝑌 , 𝑋 ) ) = 0 )
203 201 202 eqtrd ( 𝜑 → ( ( 𝑋 , ( 0g𝑊 ) ) · ( 𝑌 , 𝑋 ) ) = 0 )
204 oveq12 ( ( 𝑥 = 𝑋𝑥 = 𝑋 ) → ( 𝑥 , 𝑥 ) = ( 𝑋 , 𝑋 ) )
205 204 anidms ( 𝑥 = 𝑋 → ( 𝑥 , 𝑥 ) = ( 𝑋 , 𝑋 ) )
206 205 breq2d ( 𝑥 = 𝑋 → ( 0 ≤ ( 𝑥 , 𝑥 ) ↔ 0 ≤ ( 𝑋 , 𝑋 ) ) )
207 206 48 12 rspcdva ( 𝜑 → 0 ≤ ( 𝑋 , 𝑋 ) )
208 166 29 207 192 mulge0d ( 𝜑 → 0 ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
209 203 208 eqbrtrd ( 𝜑 → ( ( 𝑋 , ( 0g𝑊 ) ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
210 16 197 209 pm2.61ne ( 𝜑 → ( ( 𝑋 , 𝑌 ) · ( 𝑌 , 𝑋 ) ) ≤ ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
211 166 207 resqrtcld ( 𝜑 → ( √ ‘ ( 𝑋 , 𝑋 ) ) ∈ ℝ )
212 211 recnd ( 𝜑 → ( √ ‘ ( 𝑋 , 𝑋 ) ) ∈ ℂ )
213 29 192 resqrtcld ( 𝜑 → ( √ ‘ ( 𝑌 , 𝑌 ) ) ∈ ℝ )
214 213 recnd ( 𝜑 → ( √ ‘ ( 𝑌 , 𝑌 ) ) ∈ ℂ )
215 212 214 sqmuld ( 𝜑 → ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ↑ 2 ) = ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) ↑ 2 ) · ( ( √ ‘ ( 𝑌 , 𝑌 ) ) ↑ 2 ) ) )
216 167 sqsqrtd ( 𝜑 → ( ( √ ‘ ( 𝑋 , 𝑋 ) ) ↑ 2 ) = ( 𝑋 , 𝑋 ) )
217 30 sqsqrtd ( 𝜑 → ( ( √ ‘ ( 𝑌 , 𝑌 ) ) ↑ 2 ) = ( 𝑌 , 𝑌 ) )
218 216 217 oveq12d ( 𝜑 → ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) ↑ 2 ) · ( ( √ ‘ ( 𝑌 , 𝑌 ) ) ↑ 2 ) ) = ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
219 215 218 eqtrd ( 𝜑 → ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ↑ 2 ) = ( ( 𝑋 , 𝑋 ) · ( 𝑌 , 𝑌 ) ) )
220 210 171 219 3brtr4d ( 𝜑 → ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ↑ 2 ) ≤ ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ↑ 2 ) )
221 211 213 remulcld ( 𝜑 → ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ∈ ℝ )
222 22 absge0d ( 𝜑 → 0 ≤ ( abs ‘ ( 𝑋 , 𝑌 ) ) )
223 166 207 sqrtge0d ( 𝜑 → 0 ≤ ( √ ‘ ( 𝑋 , 𝑋 ) ) )
224 29 192 sqrtge0d ( 𝜑 → 0 ≤ ( √ ‘ ( 𝑌 , 𝑌 ) ) )
225 211 213 223 224 mulge0d ( 𝜑 → 0 ≤ ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) )
226 172 221 222 225 le2sqd ( 𝜑 → ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ↔ ( ( abs ‘ ( 𝑋 , 𝑌 ) ) ↑ 2 ) ≤ ( ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) ↑ 2 ) ) )
227 220 226 mpbird ( 𝜑 → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) )
228 lmodgrp ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
229 51 228 syl ( 𝜑𝑊 ∈ Grp )
230 1 10 2 6 tcphnmval ( ( 𝑊 ∈ Grp ∧ 𝑋𝑉 ) → ( 𝑁𝑋 ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )
231 229 12 230 syl2anc ( 𝜑 → ( 𝑁𝑋 ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )
232 1 10 2 6 tcphnmval ( ( 𝑊 ∈ Grp ∧ 𝑌𝑉 ) → ( 𝑁𝑌 ) = ( √ ‘ ( 𝑌 , 𝑌 ) ) )
233 229 13 232 syl2anc ( 𝜑 → ( 𝑁𝑌 ) = ( √ ‘ ( 𝑌 , 𝑌 ) ) )
234 231 233 oveq12d ( 𝜑 → ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) = ( ( √ ‘ ( 𝑋 , 𝑋 ) ) · ( √ ‘ ( 𝑌 , 𝑌 ) ) ) )
235 227 234 breqtrrd ( 𝜑 → ( abs ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁𝑋 ) · ( 𝑁𝑌 ) ) )