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

Theorem cdj1i 28482
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 10342 . . . . . . 7 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → 𝑤 ≠ 0)
2 rereccl 10592 . . . . . . 7 ((𝑤 ∈ ℝ ∧ 𝑤 ≠ 0) → (1 / 𝑤) ∈ ℝ)
31, 2syldan 485 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → (1 / 𝑤) ∈ ℝ)
43adantrr 748 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → (1 / 𝑤) ∈ ℝ)
5 recgt0 10716 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → 0 < (1 / 𝑤))
65adantrr 748 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → 0 < (1 / 𝑤))
7 1red 9911 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ∈ ℝ)
8 1re 9895 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
9 neg1cn 10971 . . . . . . . . . . . . . . . . . . . . 21 -1 ∈ ℂ
10 cdj1.2 . . . . . . . . . . . . . . . . . . . . . 22 𝐵S
1110sheli 27261 . . . . . . . . . . . . . . . . . . . . 21 (𝑧𝐵𝑧 ∈ ℋ)
12 hvmulcl 27060 . . . . . . . . . . . . . . . . . . . . 21 ((-1 ∈ ℂ ∧ 𝑧 ∈ ℋ) → (-1 · 𝑧) ∈ ℋ)
139, 11, 12sylancr 693 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐵 → (-1 · 𝑧) ∈ ℋ)
14 normcl 27172 . . . . . . . . . . . . . . . . . . . 20 ((-1 · 𝑧) ∈ ℋ → (norm‘(-1 · 𝑧)) ∈ ℝ)
1513, 14syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → (norm‘(-1 · 𝑧)) ∈ ℝ)
1615adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(-1 · 𝑧)) ∈ ℝ)
17 readdcl 9875 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ (norm‘(-1 · 𝑧)) ∈ ℝ) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
188, 16, 17sylancr 693 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
1918adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) ∈ ℝ)
20 cdj1.1 . . . . . . . . . . . . . . . . . . . . . 22 𝐴S
2120sheli 27261 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐴𝑦 ∈ ℋ)
22 hvsubcl 27064 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 𝑧) ∈ ℋ)
2321, 11, 22syl2an 492 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝐴𝑧𝐵) → (𝑦 𝑧) ∈ ℋ)
24 normcl 27172 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 𝑧) ∈ ℋ → (norm‘(𝑦 𝑧)) ∈ ℝ)
2523, 24syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℝ)
26 remulcl 9877 . . . . . . . . . . . . . . . . . . 19 ((𝑤 ∈ ℝ ∧ (norm‘(𝑦 𝑧)) ∈ ℝ) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2725, 26sylan2 489 . . . . . . . . . . . . . . . . . 18 ((𝑤 ∈ ℝ ∧ (𝑦𝐴𝑧𝐵)) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2827anassrs 677 . . . . . . . . . . . . . . . . 17 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
2928adantr 479 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
30 normge0 27173 . . . . . . . . . . . . . . . . . . 19 ((-1 · 𝑧) ∈ ℋ → 0 ≤ (norm‘(-1 · 𝑧)))
3113, 30syl 17 . . . . . . . . . . . . . . . . . 18 (𝑧𝐵 → 0 ≤ (norm‘(-1 · 𝑧)))
32 addge01 10387 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ (norm‘(-1 · 𝑧)) ∈ ℝ) → (0 ≤ (norm‘(-1 · 𝑧)) ↔ 1 ≤ (1 + (norm‘(-1 · 𝑧)))))
338, 32mpan 701 . . . . . . . . . . . . . . . . . . 19 ((norm‘(-1 · 𝑧)) ∈ ℝ → (0 ≤ (norm‘(-1 · 𝑧)) ↔ 1 ≤ (1 + (norm‘(-1 · 𝑧)))))
3433biimpa 499 . . . . . . . . . . . . . . . . . 18 (((norm‘(-1 · 𝑧)) ∈ ℝ ∧ 0 ≤ (norm‘(-1 · 𝑧))) → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
3515, 31, 34syl2anc 690 . . . . . . . . . . . . . . . . 17 (𝑧𝐵 → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
3635ad2antlr 758 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ≤ (1 + (norm‘(-1 · 𝑧))))
37 shmulcl 27265 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵S ∧ -1 ∈ ℂ ∧ 𝑧𝐵) → (-1 · 𝑧) ∈ 𝐵)
3810, 9, 37mp3an12 1405 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝐵 → (-1 · 𝑧) ∈ 𝐵)
39 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (-1 · 𝑧) → (norm𝑣) = (norm‘(-1 · 𝑧)))
4039oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (-1 · 𝑧) → ((norm𝑦) + (norm𝑣)) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
41 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑣 = (-1 · 𝑧) → (𝑦 + 𝑣) = (𝑦 + (-1 · 𝑧)))
4241fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (-1 · 𝑧) → (norm‘(𝑦 + 𝑣)) = (norm‘(𝑦 + (-1 · 𝑧))))
4342oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (-1 · 𝑧) → (𝑤 · (norm‘(𝑦 + 𝑣))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
4440, 43breq12d 4590 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (-1 · 𝑧) → (((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ↔ ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4544rspcv 3277 . . . . . . . . . . . . . . . . . . . 20 ((-1 · 𝑧) ∈ 𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4638, 45syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑧𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧))))))
4746imp 443 . . . . . . . . . . . . . . . . . 18 ((𝑧𝐵 ∧ ∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
4847ad2ant2lr 779 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → ((norm𝑦) + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
49 oveq1 6534 . . . . . . . . . . . . . . . . . . 19 (1 = (norm𝑦) → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
5049eqcoms 2617 . . . . . . . . . . . . . . . . . 18 ((norm𝑦) = 1 → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
5150ad2antll 760 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) = ((norm𝑦) + (norm‘(-1 · 𝑧))))
52 hvsubval 27063 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 𝑧) = (𝑦 + (-1 · 𝑧)))
5321, 11, 52syl2an 492 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝑧𝐵) → (𝑦 𝑧) = (𝑦 + (-1 · 𝑧)))
5453fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) = (norm‘(𝑦 + (-1 · 𝑧))))
5554oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝐴𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5655adantll 745 . . . . . . . . . . . . . . . . . 18 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5756adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (𝑤 · (norm‘(𝑦 𝑧))) = (𝑤 · (norm‘(𝑦 + (-1 · 𝑧)))))
5848, 51, 573brtr4d 4609 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 + (norm‘(-1 · 𝑧))) ≤ (𝑤 · (norm‘(𝑦 𝑧))))
597, 19, 29, 36, 58letrd 10045 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧))))
6059ex 448 . . . . . . . . . . . . . 14 (((𝑤 ∈ ℝ ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧)))))
6160adantllr 750 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → 1 ≤ (𝑤 · (norm‘(𝑦 𝑧)))))
62 simplll 793 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ∈ ℝ)
6323adantll 745 . . . . . . . . . . . . . . . 16 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑦 𝑧) ∈ ℋ)
6463, 24syl 17 . . . . . . . . . . . . . . 15 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℝ)
6562, 64, 26syl2anc 690 . . . . . . . . . . . . . 14 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ)
66 simpllr 794 . . . . . . . . . . . . . 14 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 0 < 𝑤)
67 lediv1 10737 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ ∧ (𝑤 ∈ ℝ ∧ 0 < 𝑤)) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
688, 67mp3an1 1402 . . . . . . . . . . . . . 14 (((𝑤 · (norm‘(𝑦 𝑧))) ∈ ℝ ∧ (𝑤 ∈ ℝ ∧ 0 < 𝑤)) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
6965, 62, 66, 68syl12anc 1315 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (1 ≤ (𝑤 · (norm‘(𝑦 𝑧))) ↔ (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
7061, 69sylibd 227 . . . . . . . . . . . 12 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1) → (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤)))
7170imp 443 . . . . . . . . . . 11 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 / 𝑤) ≤ ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤))
7225recnd 9924 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℂ)
7372adantll 745 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → (norm‘(𝑦 𝑧)) ∈ ℂ)
74 recn 9882 . . . . . . . . . . . . . 14 (𝑤 ∈ ℝ → 𝑤 ∈ ℂ)
7574ad3antrrr 761 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ∈ ℂ)
761ad2antrr 757 . . . . . . . . . . . . 13 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → 𝑤 ≠ 0)
7773, 75, 76divcan3d 10655 . . . . . . . . . . . 12 ((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) → ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤) = (norm‘(𝑦 𝑧)))
7877adantr 479 . . . . . . . . . . 11 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → ((𝑤 · (norm‘(𝑦 𝑧))) / 𝑤) = (norm‘(𝑦 𝑧)))
7971, 78breqtrd 4603 . . . . . . . . . 10 (((((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) ∧ 𝑧𝐵) ∧ (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) ∧ (norm𝑦) = 1)) → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))
8079exp43 637 . . . . . . . . 9 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (𝑧𝐵 → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8180com23 83 . . . . . . . 8 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → (𝑧𝐵 → ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8281ralrimdv 2950 . . . . . . 7 (((𝑤 ∈ ℝ ∧ 0 < 𝑤) ∧ 𝑦𝐴) → (∀𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ∀𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
8382ralimdva 2944 . . . . . 6 ((𝑤 ∈ ℝ ∧ 0 < 𝑤) → (∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))) → ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
8483impr 646 . . . . 5 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))
854, 6, 84jca32 555 . . . 4 ((𝑤 ∈ ℝ ∧ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣))))) → ((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
8685ex 448 . . 3 (𝑤 ∈ ℝ → ((0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))))
87 breq2 4581 . . . . 5 (𝑥 = (1 / 𝑤) → (0 < 𝑥 ↔ 0 < (1 / 𝑤)))
88 breq1 4580 . . . . . . 7 (𝑥 = (1 / 𝑤) → (𝑥 ≤ (norm‘(𝑦 𝑧)) ↔ (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))
8988imbi2d 328 . . . . . 6 (𝑥 = (1 / 𝑤) → (((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))) ↔ ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
90892ralbidv 2971 . . . . 5 (𝑥 = (1 / 𝑤) → (∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))) ↔ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧)))))
9187, 90anbi12d 742 . . . 4 (𝑥 = (1 / 𝑤) → ((0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))) ↔ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))))
9291rspcev 3281 . . 3 (((1 / 𝑤) ∈ ℝ ∧ (0 < (1 / 𝑤) ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → (1 / 𝑤) ≤ (norm‘(𝑦 𝑧))))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))))
9386, 92syl6 34 . 2 (𝑤 ∈ ℝ → ((0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧))))))
9493rexlimiv 3008 1 (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦𝐴𝑣𝐵 ((norm𝑦) + (norm𝑣)) ≤ (𝑤 · (norm‘(𝑦 + 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦𝐴𝑧𝐵 ((norm𝑦) = 1 → 𝑥 ≤ (norm‘(𝑦 𝑧)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896   class class class wbr 4577  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  -cneg 10118   / cdiv 10533  chil 26966   + cva 26967   · csm 26968  normcno 26970   cmv 26972   S csh 26975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-hilex 27046  ax-hfvadd 27047  ax-hv0cl 27050  ax-hfvmul 27052  ax-hvmul0 27057  ax-hfi 27126  ax-his1 27129  ax-his3 27131  ax-his4 27132
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-sup 8208  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-rp 11665  df-seq 12619  df-exp 12678  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-hnorm 27015  df-hvsub 27018  df-sh 27254
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator