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 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
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 ⊢ ( 𝜑 → 𝐹 = ( ℂfld ↾s 𝐾 ) )
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 ⊢ ( 𝜑 → ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) ) )
58 9 fvexi ⊢ 𝐾 ∈ V
59 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
60 cnfldcj ⊢ ∗ = ( *𝑟 ‘ ℂfld )
61 59 60 ressstarv ⊢ ( 𝐾 ∈ V → ∗ = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) ) )
62 58 61 ax-mp ⊢ ∗ = ( *𝑟 ‘ ( ℂfld ↾s 𝐾 ) )
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 ‘ 𝑊 ) ) → 𝐹 = ( ℂfld ↾s 𝐾 ) )
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 ‘ ( ℂfld ↾s 𝐾 ) ) )
107 cnfldadd ⊢ + = ( +g ‘ ℂfld )
108 59 107 ressplusg ⊢ ( 𝐾 ∈ V → + = ( +g ‘ ( ℂfld ↾s 𝐾 ) ) )
109 58 108 ax-mp ⊢ + = ( +g ‘ ( ℂfld ↾s 𝐾 ) )
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 ‘ ( ℂfld ↾s 𝐾 ) ) )
116 cnfldmul ⊢ · = ( .r ‘ ℂfld )
117 59 116 ressmulr ⊢ ( 𝐾 ∈ V → · = ( .r ‘ ( ℂfld ↾s 𝐾 ) ) )
118 58 117 ax-mp ⊢ · = ( .r ‘ ( ℂfld ↾s 𝐾 ) )
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 ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) )