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 eqtrid ⊒ ( ( πœ‘ ∧ π‘Œ β‰  ( 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 eqtrid ⊒ ( ( πœ‘ ∧ π‘Œ β‰  ( 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 eqtrid ⊒ ( ( πœ‘ ∧ π‘Œ β‰  ( 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 β€˜ ( 𝑋 , π‘Œ ) ) ≀ ( ( 𝑁 β€˜ 𝑋 ) Β· ( 𝑁 β€˜ π‘Œ ) ) )