Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈
CPreHilOLD) |
2 | | phnv 28895 |
. . . . . . . 8
⊢ (𝑈 ∈ CPreHilOLD
→ 𝑈 ∈
NrmCVec) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ NrmCVec) |
4 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑈 ∈ NrmCVec) |
5 | | minveco.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
6 | 5 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝐴 ∈ 𝑋) |
7 | | inss1 4143 |
. . . . . . . . 9
⊢
((SubSp‘𝑈)
∩ CBan) ⊆ (SubSp‘𝑈) |
8 | | minveco.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) |
9 | 7, 8 | sseldi 3899 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈)) |
10 | | minveco.x |
. . . . . . . . 9
⊢ 𝑋 = (BaseSet‘𝑈) |
11 | | minveco.y |
. . . . . . . . 9
⊢ 𝑌 = (BaseSet‘𝑊) |
12 | | eqid 2737 |
. . . . . . . . 9
⊢
(SubSp‘𝑈) =
(SubSp‘𝑈) |
13 | 10, 11, 12 | sspba 28808 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋) |
14 | 3, 9, 13 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ 𝑋) |
15 | 14 | sselda 3901 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
16 | | minveco.m |
. . . . . . 7
⊢ 𝑀 = ( −𝑣
‘𝑈) |
17 | | minveco.n |
. . . . . . 7
⊢ 𝑁 =
(normCV‘𝑈) |
18 | | minveco.d |
. . . . . . 7
⊢ 𝐷 = (IndMet‘𝑈) |
19 | 10, 16, 17, 18 | imsdval 28767 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐴𝐷𝑥) = (𝑁‘(𝐴𝑀𝑥))) |
20 | 4, 6, 15, 19 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴𝐷𝑥) = (𝑁‘(𝐴𝑀𝑥))) |
21 | 20 | oveq1d 7228 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝐴𝐷𝑥)↑2) = ((𝑁‘(𝐴𝑀𝑥))↑2)) |
22 | | minveco.s |
. . . . . . . 8
⊢ 𝑆 = inf(𝑅, ℝ, < ) |
23 | | minveco.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘𝐷) |
24 | | minveco.r |
. . . . . . . . . . . 12
⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
25 | 10, 16, 17, 11, 1, 8, 5, 18, 23, 24 | minvecolem1 28955 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
26 | 25 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
27 | 26 | simp1d 1144 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑅 ⊆ ℝ) |
28 | 26 | simp2d 1145 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑅 ≠ ∅) |
29 | | 0red 10836 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ∈ ℝ) |
30 | 26 | simp3d 1146 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) |
31 | | breq1 5056 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
32 | 31 | ralbidv 3118 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
33 | 32 | rspcev 3537 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
34 | 29, 30, 33 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) |
35 | | infrecl 11814 |
. . . . . . . . 9
⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈
ℝ) |
36 | 27, 28, 34, 35 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → inf(𝑅, ℝ, < ) ∈
ℝ) |
37 | 22, 36 | eqeltrid 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ ℝ) |
38 | 37 | resqcld 13817 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆↑2) ∈ ℝ) |
39 | 38 | recnd 10861 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑆↑2) ∈ ℂ) |
40 | 39 | addid1d 11032 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑆↑2) + 0) = (𝑆↑2)) |
41 | 21, 40 | breq12d 5066 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ((𝑁‘(𝐴𝑀𝑥))↑2) ≤ (𝑆↑2))) |
42 | 10, 16 | nvmcl 28727 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝐴𝑀𝑥) ∈ 𝑋) |
43 | 4, 6, 15, 42 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝐴𝑀𝑥) ∈ 𝑋) |
44 | 10, 17 | nvcl 28742 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑥) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑥)) ∈ ℝ) |
45 | 4, 43, 44 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (𝑁‘(𝐴𝑀𝑥)) ∈ ℝ) |
46 | 10, 17 | nvge0 28754 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑥) ∈ 𝑋) → 0 ≤ (𝑁‘(𝐴𝑀𝑥))) |
47 | 4, 43, 46 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ (𝑁‘(𝐴𝑀𝑥))) |
48 | | infregelb 11816 |
. . . . . . 7
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤
inf(𝑅, ℝ, < )
↔ ∀𝑤 ∈
𝑅 0 ≤ 𝑤)) |
49 | 27, 28, 34, 29, 48 | syl31anc 1375 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) |
50 | 30, 49 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ inf(𝑅, ℝ, < )) |
51 | 50, 22 | breqtrrdi 5095 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → 0 ≤ 𝑆) |
52 | 45, 37, 47, 51 | le2sqd 13826 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴𝑀𝑥)) ≤ 𝑆 ↔ ((𝑁‘(𝐴𝑀𝑥))↑2) ≤ (𝑆↑2))) |
53 | 22 | breq2i 5061 |
. . . 4
⊢ ((𝑁‘(𝐴𝑀𝑥)) ≤ 𝑆 ↔ (𝑁‘(𝐴𝑀𝑥)) ≤ inf(𝑅, ℝ, < )) |
54 | | infregelb 11816 |
. . . . 5
⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ (𝑁‘(𝐴𝑀𝑥)) ∈ ℝ) → ((𝑁‘(𝐴𝑀𝑥)) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤)) |
55 | 27, 28, 34, 45, 54 | syl31anc 1375 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴𝑀𝑥)) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤)) |
56 | 53, 55 | syl5bb 286 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → ((𝑁‘(𝐴𝑀𝑥)) ≤ 𝑆 ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤)) |
57 | 41, 52, 56 | 3bitr2d 310 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑤 ∈ 𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤)) |
58 | 24 | raleqi 3323 |
. . 3
⊢
(∀𝑤 ∈
𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤) |
59 | | fvex 6730 |
. . . . 5
⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V |
60 | 59 | rgenw 3073 |
. . . 4
⊢
∀𝑦 ∈
𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V |
61 | | eqid 2737 |
. . . . 5
⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) |
62 | | breq2 5057 |
. . . . 5
⊢ (𝑤 = (𝑁‘(𝐴𝑀𝑦)) → ((𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤 ↔ (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
63 | 61, 62 | ralrnmptw 6913 |
. . . 4
⊢
(∀𝑦 ∈
𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |
64 | 60, 63 | ax-mp 5 |
. . 3
⊢
(∀𝑤 ∈
ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
65 | 58, 64 | bitri 278 |
. 2
⊢
(∀𝑤 ∈
𝑅 (𝑁‘(𝐴𝑀𝑥)) ≤ 𝑤 ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) |
66 | 57, 65 | bitrdi 290 |
1
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) |