HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cdj1i Structured version   Visualization version   GIF version

Theorem cdj1i 29649
Description: Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdj1.1 𝐴S
cdj1.2 𝐵S
Assertion
Ref Expression
cdj1i (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝐴   𝑥,𝑣,𝐵,𝑦,𝑧,𝑤
Allowed substitution hint:   𝐴(𝑣)

Proof of Theorem cdj1i
StepHypRef Expression
1 gt0ne0 10716 . . . . . . 7 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → 𝑤 ≠ 0)
2 rereccl 10966 . . . . . . 7 ((𝑤 ∈ ℝ ∧ 𝑤 ≠ 0) → (1 / 𝑤) ∈ ℝ)
31, 2syldan 580 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → (1 / 𝑤) ∈ ℝ)
43adantrr 697 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → (1 / 𝑤) ∈ ℝ)
5 recgt0 11090 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → 0 < (1 / 𝑤))
65adantrr 697 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → 0 < (1 / 𝑤))
7 1red 10278 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ∈ ℝ)
8 1re 10262 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
9 neg1cn 11347 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℂ
10 cdj1.2 . . . . . . . . . . . . . . . . . . . . . 22 𝐵S
1110sheli 28428 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝐵𝑧 ∈ ℋ)
12 hvmulcl 28227 . . . . . . . . . . . . . . . . . . . . 21 ((-1 ∈ ℂ ∧ 𝑧 ∈ ℋ) → (-1 · 𝑧) ∈ ℋ)
139, 11, 12sylancr 576 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐵 → (-1 · 𝑧) ∈ ℋ)
14 normcl 28339 . . . . . . . . . . . . . . . . . . . 20 ((-1 · 𝑧) ∈ ℋ → (norm‘(-1 · 𝑧)) ∈ ℝ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → (norm‘(-1 · 𝑧)) ∈ ℝ)
1615adantl 468 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(-1 · 𝑧)) ∈ ℝ)
17 readdcl 10242 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (norm‘(-1 · 𝑧)) ∈ ℝ) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
188, 16, 17sylancr 576 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
1918adantr 467 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
20 cdj1.1 . . . . . . . . . . . . . . . . . . . . . 22 𝐴S
2120sheli 28428 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐴𝑦 ∈ ℋ)
22 hvsubcl 28231 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 𝑧) ∈ ℋ)
2321, 11, 22syl2an 584 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝐴𝑧𝐵) → (𝑦 𝑧) ∈ ℋ)
24 normcl 28339 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 𝑧) ∈ ℋ → (norm‘(𝑦 𝑧)) ∈ ℝ)
2523, 24syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℝ)
26 remulcl 10244 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ℝ ∧ (norm‘(𝑦 𝑧)) ∈ ℝ) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2725, 26sylan2 581 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ (𝑦𝐴𝑧𝐵)) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2827anassrs 454 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2928adantr 467 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
30 normge0 28340 . . . . . . . . . . . . . . . . . . 19 ((-1 · 𝑧) ∈ ℋ → 0 ≤ (norm‘(-1 · 𝑧)))
3113, 30syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝐵 → 0 ≤ (norm‘(-1 · 𝑧)))
32 addge01 10761 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ (norm‘(-1 · 𝑧)) ∈ ℝ) → (0 ≤ (norm‘(-1 · 𝑧)) ↔ 1 ≤ (1 + (norm‘(-1 · 𝑧)))))
338, 32mpan 671 . . . . . . . . . . . . . . . . . . 19 ((norm‘(-1 · 𝑧)) ∈ ℝ → (0 ≤ (norm‘(-1 · 𝑧)) ↔ 1 ≤ (1 + (norm‘(-1 · 𝑧)))))
3433biimpa 463 . . . . . . . . . . . . . . . . . 18 (((norm‘(-1 · 𝑧)) ∈ ℝ ∧ 0 ≤ (norm‘(-1 · 𝑧))) → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
3515, 31, 34syl2anc 574 . . . . . . . . . . . . . . . . 17 (𝑧𝐵 → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
3635ad2antlr 707 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
37 shmulcl 28432 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵S ∧ -1 ∈ ℂ ∧ 𝑧𝐵) → (-1 · 𝑧) ∈ 𝐵)
3810, 9, 37mp3an12 1565 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐵 → (-1 · 𝑧) ∈ 𝐵)
39 fveq2 6348 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (-1 · 𝑧) → (norm𝑣) = (norm‘(-1 · 𝑧)))
4039oveq2d 6828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (-1 · 𝑧) → ((norm𝑦) + (norm𝑣)) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
41 oveq2 6820 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = (-1 · 𝑧) → (𝑦 + 𝑣) = (𝑦 + (-1 · 𝑧)))
4241fveq2d 6352 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (-1 · 𝑧) → (norm‘(𝑦 + 𝑣)) = (norm‘(𝑦 + (-1 · 𝑧))))
4342oveq2d 6828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (-1 · 𝑧) → (𝑤 · (norm‘(𝑦 + 𝑣))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
4440, 43breq12d 4810 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (-1 · 𝑧) → (((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ↔ ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4544rspcv 3461 . . . . . . . . . . . . . . . . . . . 20 ((-1 · 𝑧) ∈ 𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4638, 45syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4746imp 394 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵 ∧ ∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
4847ad2ant2lr 743 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
49 oveq1 6819 . . . . . . . . . . . . . . . . . . 19 (1 = (norm𝑦) → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
5049eqcoms 2782 . . . . . . . . . . . . . . . . . 18 ((norm𝑦) = 1 → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
5150ad2antll 709 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
52 hvsubval 28230 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 𝑧) = (𝑦 + (-1 · 𝑧)))
5321, 11, 52syl2an 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝑧𝐵) → (𝑦 𝑧) = (𝑦 + (-1 · 𝑧)))
5453fveq2d 6352 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) = (norm‘(𝑦 + (-1 · 𝑧))))
5554oveq2d 6828 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝐴𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5655adantll 694 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5756adantr 467 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5848, 51, 573brtr4d 4829 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 𝑧))))
597, 19, 29, 36, 58letrd 10417 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧))))
6059ex 398 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧)))))
6160adantllr 699 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧)))))
62 simplll 780 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ∈ ℝ)
6323adantll 694 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑦 𝑧) ∈ ℋ)
6463, 24syl 17 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℝ)
6562, 64, 26syl2anc 574 . . . . . . . . . . . . . 14 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
66 simpllr 782 . . . . . . . . . . . . . 14 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 0 < 𝑤)
67 lediv1 11111 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ ∧ (𝑤 ∈ ℝ ∧ 0 < 𝑤)) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
688, 67mp3an1 1562 . . . . . . . . . . . . . 14 (((𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ ∧ (𝑤 ∈ ℝ ∧ 0 < 𝑤)) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
6965, 62, 66, 68syl12anc 854 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
7061, 69sylibd 230 . . . . . . . . . . . 12 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
7170imp 394 . . . . . . . . . . 11 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤))
7225recnd 10291 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℂ)
7372adantll 694 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℂ)
74 recn 10249 . . . . . . . . . . . . . 14 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
7574ad3antrrr 710 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ∈ ℂ)
761ad2antrr 706 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ≠ 0)
7773, 75, 76divcan3d 11029 . . . . . . . . . . . 12 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤) = (norm‘(𝑦 𝑧)))
7877adantr 467 . . . . . . . . . . 11 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤) = (norm‘(𝑦 𝑧)))
7971, 78breqtrd 4823 . . . . . . . . . 10 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))
8079exp43 424 . . . . . . . . 9 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (𝑧𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8180com23 86 . . . . . . . 8 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → (𝑧𝐵 → ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8281ralrimdv 3120 . . . . . . 7 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ∀𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
8382ralimdva 3114 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → (∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
8483impr 443 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))
854, 6, 84jca32 506 . . . 4 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → ((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8685ex 398 . . 3 (𝑤 ∈ ℝ → ((0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))))
87 breq2 4801 . . . . 5 (𝑥 = (1 / 𝑤) → (0 < 𝑥 ↔ 0 < (1 / 𝑤)))
88 breq1 4800 . . . . . . 7 (𝑥 = (1 / 𝑤) → (𝑥 ≤ (norm‘(𝑦 𝑧)) ↔ (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))
8988imbi2d 330 . . . . . 6 (𝑥 = (1 / 𝑤) → (((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))) ↔ ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
90892ralbidv 3141 . . . . 5 (𝑥 = (1 / 𝑤) → (∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))) ↔ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
9187, 90anbi12d 617 . . . 4 (𝑥 = (1 / 𝑤) → ((0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))) ↔ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
9291rspcev 3465 . . 3 (((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))))
9386, 92syl6 35 . 2 (𝑤 ∈ ℝ → ((0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))))))
9493rexlimiv 3179 1 (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383   = wceq 1634  wcel 2148  wne 2946  wral 3064  wrex 3065   class class class wbr 4797  cfv 6042  (class class class)co 6812  cc 10157  cr 10158  0cc0 10159  1c1 10160   + caddc 10162   · cmul 10164   < clt 10297  cle 10298  -cneg 10490   / cdiv 10907  chil 28133   + cva 28134   · csm 28135  normcno 28137   cmv 28139   S csh 28142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117  ax-cnex 10215  ax-resscn 10216  ax-1cn 10217  ax-icn 10218  ax-addcl 10219  ax-addrcl 10220  ax-mulcl 10221  ax-mulrcl 10222  ax-mulcom 10223  ax-addass 10224  ax-mulass 10225  ax-distr 10226  ax-i2m1 10227  ax-1ne0 10228  ax-1rid 10229  ax-rnegex 10230  ax-rrecex 10231  ax-cnre 10232  ax-pre-lttri 10233  ax-pre-lttrn 10234  ax-pre-ltadd 10235  ax-pre-mulgt0 10236  ax-pre-sup 10237  ax-hilex 28213  ax-hfvadd 28214  ax-hv0cl 28217  ax-hfvmul 28219  ax-hvmul0 28224  ax-hfi 28293  ax-his1 28296  ax-his3 28298  ax-his4 28299
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-lim 5882  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-ov 6815  df-oprab 6816  df-mpt2 6817  df-om 7234  df-2nd 7337  df-wrecs 7580  df-recs 7642  df-rdg 7680  df-er 7917  df-en 8131  df-dom 8132  df-sdom 8133  df-sup 8525  df-pnf 10299  df-mnf 10300  df-xr 10301  df-ltxr 10302  df-le 10303  df-sub 10491  df-neg 10492  df-div 10908  df-nn 11244  df-2 11302  df-3 11303  df-n0 11517  df-z 11602  df-uz 11911  df-rp 12053  df-seq 13031  df-exp 13090  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-hnorm 28182  df-hvsub 28185  df-sh 28421
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator