Step | Hyp | Ref
| Expression |
1 | | pjthlem.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | | pjthlem.m |
. . . 4
⊢ − =
(-g‘𝑊) |
3 | | pjthlem.n |
. . . 4
⊢ 𝑁 = (norm‘𝑊) |
4 | | pjthlem.1 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ ℂHil) |
5 | | hlcph 22968 |
. . . . 5
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈
ℂPreHil) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ℂPreHil) |
7 | | pjthlem.2 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝐿) |
8 | | pjthlem.l |
. . . . 5
⊢ 𝐿 = (LSubSp‘𝑊) |
9 | 7, 8 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝑊)) |
10 | | pjthlem.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽)) |
11 | | hlcms 22970 |
. . . . . . 7
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp) |
12 | 4, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ CMetSp) |
13 | 1, 8 | lssss 18758 |
. . . . . . 7
⊢ (𝑈 ∈ 𝐿 → 𝑈 ⊆ 𝑉) |
14 | 7, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ 𝑉) |
15 | | eqid 2610 |
. . . . . . 7
⊢ (𝑊 ↾s 𝑈) = (𝑊 ↾s 𝑈) |
16 | | pjthlem.j |
. . . . . . 7
⊢ 𝐽 = (TopOpen‘𝑊) |
17 | 15, 1, 16 | cmsss 22955 |
. . . . . 6
⊢ ((𝑊 ∈ CMetSp ∧ 𝑈 ⊆ 𝑉) → ((𝑊 ↾s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽))) |
18 | 12, 14, 17 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑊 ↾s 𝑈) ∈ CMetSp ↔ 𝑈 ∈ (Clsd‘𝐽))) |
19 | 10, 18 | mpbird 246 |
. . . 4
⊢ (𝜑 → (𝑊 ↾s 𝑈) ∈ CMetSp) |
20 | | pjthlem.4 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
21 | 1, 2, 3, 6, 9, 19,
20 | minvec 23015 |
. . 3
⊢ (𝜑 → ∃!𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
22 | | reurex 3137 |
. . 3
⊢
(∃!𝑥 ∈
𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
23 | 21, 22 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
24 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ ℂPreHil) |
25 | | cphlmod 22782 |
. . . . . 6
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
LMod) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ LMod) |
27 | | lmodabl 18733 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
28 | 26, 27 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Abel) |
29 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ 𝐿) |
30 | 29, 13 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ⊆ 𝑉) |
31 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑈) |
32 | 30, 31 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑥 ∈ 𝑉) |
33 | 20 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ 𝑉) |
34 | | pjthlem.p |
. . . . 5
⊢ + =
(+g‘𝑊) |
35 | 1, 34, 2 | ablpncan3 18045 |
. . . 4
⊢ ((𝑊 ∈ Abel ∧ (𝑥 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) → (𝑥 + (𝐴 − 𝑥)) = 𝐴) |
36 | 28, 32, 33, 35 | syl12anc 1316 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) = 𝐴) |
37 | 8 | lsssssubg 18779 |
. . . . . 6
⊢ (𝑊 ∈ LMod → 𝐿 ⊆ (SubGrp‘𝑊)) |
38 | 26, 37 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐿 ⊆ (SubGrp‘𝑊)) |
39 | 38, 29 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑈 ∈ (SubGrp‘𝑊)) |
40 | | cphphl 22779 |
. . . . . . 7
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
PreHil) |
41 | 24, 40 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ PreHil) |
42 | | pjthlem.o |
. . . . . . 7
⊢ 𝑂 = (ocv‘𝑊) |
43 | 1, 42, 8 | ocvlss 19835 |
. . . . . 6
⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ⊆ 𝑉) → (𝑂‘𝑈) ∈ 𝐿) |
44 | 41, 30, 43 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ 𝐿) |
45 | 38, 44 | sseldd 3569 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) |
46 | 1, 2 | lmodvsubcl 18731 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → (𝐴 − 𝑥) ∈ 𝑉) |
47 | 26, 33, 32, 46 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ 𝑉) |
48 | | pjthlem.h |
. . . . . . . 8
⊢ , =
(·𝑖‘𝑊) |
49 | 4 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂHil) |
50 | 29 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑈 ∈ 𝐿) |
51 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → (𝐴 − 𝑥) ∈ 𝑉) |
52 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑧 ∈ 𝑈) |
53 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ LMod) |
54 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑈 ∈ 𝐿) |
55 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑈) |
56 | 31 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑈) |
57 | 34, 8 | lssvacl 18775 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝐿) ∧ (𝑤 ∈ 𝑈 ∧ 𝑥 ∈ 𝑈)) → (𝑤 + 𝑥) ∈ 𝑈) |
58 | 53, 54, 55, 56, 57 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑤 + 𝑥) ∈ 𝑈) |
59 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
60 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑤 + 𝑥) → (𝐴 − 𝑦) = (𝐴 − (𝑤 + 𝑥))) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑤 + 𝑥) → (𝑁‘(𝐴 − 𝑦)) = (𝑁‘(𝐴 − (𝑤 + 𝑥)))) |
62 | 61 | breq2d 4595 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑤 + 𝑥) → ((𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) ↔ (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))) |
63 | 62 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ ((𝑤 + 𝑥) ∈ 𝑈 → (∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥))))) |
64 | 58, 59, 63 | sylc 63 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − (𝑤 + 𝑥)))) |
65 | | lmodgrp 18693 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
66 | 26, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝑊 ∈ Grp) |
67 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑊 ∈ Grp) |
68 | 33 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝐴 ∈ 𝑉) |
69 | 32 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑥 ∈ 𝑉) |
70 | 30 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → 𝑤 ∈ 𝑉) |
71 | 1, 34, 2 | grpsubsub4 17331 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Grp ∧ (𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉)) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥))) |
72 | 67, 68, 69, 70, 71 | syl13anc 1320 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → ((𝐴 − 𝑥) − 𝑤) = (𝐴 − (𝑤 + 𝑥))) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘((𝐴 − 𝑥) − 𝑤)) = (𝑁‘(𝐴 − (𝑤 + 𝑥)))) |
74 | 64, 73 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑤 ∈ 𝑈) → (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤))) |
75 | 74 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤))) |
76 | 75 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ∀𝑤 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘((𝐴 − 𝑥) − 𝑤))) |
77 | | eqid 2610 |
. . . . . . . 8
⊢ (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) = (((𝐴 − 𝑥) , 𝑧) / ((𝑧 , 𝑧) + 1)) |
78 | 1, 3, 34, 2, 48, 8, 49, 50, 51, 52, 76, 77 | pjthlem1 23016 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = 0) |
79 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂPreHil) |
80 | | cphclm 22797 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂPreHil →
𝑊 ∈
ℂMod) |
81 | 79, 80 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 𝑊 ∈ ℂMod) |
82 | | eqid 2610 |
. . . . . . . . 9
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
83 | 82 | clm0 22680 |
. . . . . . . 8
⊢ (𝑊 ∈ ℂMod → 0 =
(0g‘(Scalar‘𝑊))) |
84 | 81, 83 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → 0 =
(0g‘(Scalar‘𝑊))) |
85 | 78, 84 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) ∧ 𝑧 ∈ 𝑈) → ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊))) |
86 | 85 | ralrimiva 2949 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊))) |
87 | | eqid 2610 |
. . . . . 6
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
88 | 1, 48, 82, 87, 42 | elocv 19831 |
. . . . 5
⊢ ((𝐴 − 𝑥) ∈ (𝑂‘𝑈) ↔ (𝑈 ⊆ 𝑉 ∧ (𝐴 − 𝑥) ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑈 ((𝐴 − 𝑥) , 𝑧) = (0g‘(Scalar‘𝑊)))) |
89 | 30, 47, 86, 88 | syl3anbrc 1239 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝐴 − 𝑥) ∈ (𝑂‘𝑈)) |
90 | | pjthlem.s |
. . . . 5
⊢ ⊕ =
(LSSum‘𝑊) |
91 | 34, 90 | lsmelvali 17888 |
. . . 4
⊢ (((𝑈 ∈ (SubGrp‘𝑊) ∧ (𝑂‘𝑈) ∈ (SubGrp‘𝑊)) ∧ (𝑥 ∈ 𝑈 ∧ (𝐴 − 𝑥) ∈ (𝑂‘𝑈))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈))) |
92 | 39, 45, 31, 89, 91 | syl22anc 1319 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → (𝑥 + (𝐴 − 𝑥)) ∈ (𝑈 ⊕ (𝑂‘𝑈))) |
93 | 36, 92 | eqeltrrd 2689 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑈 ∧ ∀𝑦 ∈ 𝑈 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))) → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈))) |
94 | 23, 93 | rexlimddv 3017 |
1
⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈))) |