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 ‘ ( 𝑋 , 𝑌 ) ) ≤ ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) ) |