Metamath Proof Explorer

Theorem cdj1i

Description: Two ways to express " A and B are completely disjoint subspaces." (1) => (2) in Lemma 5 of Holland p. 1520. (Contributed by NM, 21-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj1.1 ⊢ A ∈ S ℋ
cdj1.2 ⊢ B ∈ S ℋ
Assertion cdj1i ⊢ ∃ w ∈ ℝ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∃ x ∈ ℝ 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z

Proof

Step Hyp Ref Expression
1 cdj1.1 ⊢ A ∈ S ℋ
2 cdj1.2 ⊢ B ∈ S ℋ
3 gt0ne0 ⊢ w ∈ ℝ ∧ 0 < w → w ≠ 0
4 rereccl ⊢ w ∈ ℝ ∧ w ≠ 0 → 1 w ∈ ℝ
5 3 4 syldan ⊢ w ∈ ℝ ∧ 0 < w → 1 w ∈ ℝ
6 5 adantrr ⊢ w ∈ ℝ ∧ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → 1 w ∈ ℝ
7 recgt0 ⊢ w ∈ ℝ ∧ 0 < w → 0 < 1 w
8 7 adantrr ⊢ w ∈ ℝ ∧ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → 0 < 1 w
9 1red ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 ∈ ℝ
10 1re ⊢ 1 ∈ ℝ
11 neg1cn ⊢ − 1 ∈ ℂ
12 2 sheli ⊢ z ∈ B → z ∈ ℋ
13 hvmulcl ⊢ − 1 ∈ ℂ ∧ z ∈ ℋ → -1 ⋅ ℎ z ∈ ℋ
14 11 12 13 sylancr ⊢ z ∈ B → -1 ⋅ ℎ z ∈ ℋ
15 normcl ⊢ -1 ⋅ ℎ z ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
16 14 15 syl ⊢ z ∈ B → norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
17 16 adantl ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
18 readdcl ⊢ 1 ∈ ℝ ∧ norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ → 1 + norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
19 10 17 18 sylancr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → 1 + norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
20 19 adantr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 + norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ
21 1 sheli ⊢ y ∈ A → y ∈ ℋ
22 hvsubcl ⊢ y ∈ ℋ ∧ z ∈ ℋ → y - ℎ z ∈ ℋ
23 21 12 22 syl2an ⊢ y ∈ A ∧ z ∈ B → y - ℎ z ∈ ℋ
24 normcl ⊢ y - ℎ z ∈ ℋ → norm ℎ ⁡ y - ℎ z ∈ ℝ
25 23 24 syl ⊢ y ∈ A ∧ z ∈ B → norm ℎ ⁡ y - ℎ z ∈ ℝ
26 remulcl ⊢ w ∈ ℝ ∧ norm ℎ ⁡ y - ℎ z ∈ ℝ → w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ
27 25 26 sylan2 ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ
28 27 anassrs ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ
29 28 adantr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ
30 normge0 ⊢ -1 ⋅ ℎ z ∈ ℋ → 0 ≤ norm ℎ ⁡ -1 ⋅ ℎ z
31 14 30 syl ⊢ z ∈ B → 0 ≤ norm ℎ ⁡ -1 ⋅ ℎ z
32 addge01 ⊢ 1 ∈ ℝ ∧ norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ → 0 ≤ norm ℎ ⁡ -1 ⋅ ℎ z ↔ 1 ≤ 1 + norm ℎ ⁡ -1 ⋅ ℎ z
33 10 32 mpan ⊢ norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ → 0 ≤ norm ℎ ⁡ -1 ⋅ ℎ z ↔ 1 ≤ 1 + norm ℎ ⁡ -1 ⋅ ℎ z
34 33 biimpa ⊢ norm ℎ ⁡ -1 ⋅ ℎ z ∈ ℝ ∧ 0 ≤ norm ℎ ⁡ -1 ⋅ ℎ z → 1 ≤ 1 + norm ℎ ⁡ -1 ⋅ ℎ z
35 16 31 34 syl2anc ⊢ z ∈ B → 1 ≤ 1 + norm ℎ ⁡ -1 ⋅ ℎ z
36 35 ad2antlr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 ≤ 1 + norm ℎ ⁡ -1 ⋅ ℎ z
37 shmulcl ⊢ B ∈ S ℋ ∧ − 1 ∈ ℂ ∧ z ∈ B → -1 ⋅ ℎ z ∈ B
38 2 11 37 mp3an12 ⊢ z ∈ B → -1 ⋅ ℎ z ∈ B
39 fveq2 ⊢ v = -1 ⋅ ℎ z → norm ℎ ⁡ v = norm ℎ ⁡ -1 ⋅ ℎ z
40 39 oveq2d ⊢ v = -1 ⋅ ℎ z → norm ℎ ⁡ y + norm ℎ ⁡ v = norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z
41 oveq2 ⊢ v = -1 ⋅ ℎ z → y + ℎ v = y + ℎ -1 ⋅ ℎ z
42 41 fveq2d ⊢ v = -1 ⋅ ℎ z → norm ℎ ⁡ y + ℎ v = norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
43 42 oveq2d ⊢ v = -1 ⋅ ℎ z → w ⁢ norm ℎ ⁡ y + ℎ v = w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
44 40 43 breq12d ⊢ v = -1 ⋅ ℎ z → norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ↔ norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
45 44 rspcv ⊢ -1 ⋅ ℎ z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
46 38 45 syl ⊢ z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
47 46 imp ⊢ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
48 47 ad2ant2lr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
49 oveq1 ⊢ 1 = norm ℎ ⁡ y → 1 + norm ℎ ⁡ -1 ⋅ ℎ z = norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z
50 49 eqcoms ⊢ norm ℎ ⁡ y = 1 → 1 + norm ℎ ⁡ -1 ⋅ ℎ z = norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z
51 50 ad2antll ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 + norm ℎ ⁡ -1 ⋅ ℎ z = norm ℎ ⁡ y + norm ℎ ⁡ -1 ⋅ ℎ z
52 hvsubval ⊢ y ∈ ℋ ∧ z ∈ ℋ → y - ℎ z = y + ℎ -1 ⋅ ℎ z
53 21 12 52 syl2an ⊢ y ∈ A ∧ z ∈ B → y - ℎ z = y + ℎ -1 ⋅ ℎ z
54 53 fveq2d ⊢ y ∈ A ∧ z ∈ B → norm ℎ ⁡ y - ℎ z = norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
55 54 oveq2d ⊢ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z = w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
56 55 adantll ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z = w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
57 56 adantr ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → w ⁢ norm ℎ ⁡ y - ℎ z = w ⁢ norm ℎ ⁡ y + ℎ -1 ⋅ ℎ z
58 48 51 57 3brtr4d ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 + norm ℎ ⁡ -1 ⋅ ℎ z ≤ w ⁢ norm ℎ ⁡ y - ℎ z
59 9 20 29 36 58 letrd ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z
60 59 ex ⊢ w ∈ ℝ ∧ y ∈ A ∧ z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z
61 60 adantllr ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z
62 simplll ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → w ∈ ℝ
63 23 adantll ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → y - ℎ z ∈ ℋ
64 63 24 syl ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → norm ℎ ⁡ y - ℎ z ∈ ℝ
65 62 64 26 syl2anc ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ
66 simpllr ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → 0 < w
67 lediv1 ⊢ 1 ∈ ℝ ∧ w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ ∧ w ∈ ℝ ∧ 0 < w → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z ↔ 1 w ≤ w ⁢ norm ℎ ⁡ y - ℎ z w
68 10 67 mp3an1 ⊢ w ⁢ norm ℎ ⁡ y - ℎ z ∈ ℝ ∧ w ∈ ℝ ∧ 0 < w → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z ↔ 1 w ≤ w ⁢ norm ℎ ⁡ y - ℎ z w
69 65 62 66 68 syl12anc ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → 1 ≤ w ⁢ norm ℎ ⁡ y - ℎ z ↔ 1 w ≤ w ⁢ norm ℎ ⁡ y - ℎ z w
70 61 69 sylibd ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 w ≤ w ⁢ norm ℎ ⁡ y - ℎ z w
71 70 imp ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 w ≤ w ⁢ norm ℎ ⁡ y - ℎ z w
72 25 recnd ⊢ y ∈ A ∧ z ∈ B → norm ℎ ⁡ y - ℎ z ∈ ℂ
73 72 adantll ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → norm ℎ ⁡ y - ℎ z ∈ ℂ
74 recn ⊢ w ∈ ℝ → w ∈ ℂ
75 74 ad3antrrr ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → w ∈ ℂ
76 3 ad2antrr ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → w ≠ 0
77 73 75 76 divcan3d ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B → w ⁢ norm ℎ ⁡ y - ℎ z w = norm ℎ ⁡ y - ℎ z
78 77 adantr ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → w ⁢ norm ℎ ⁡ y - ℎ z w = norm ℎ ⁡ y - ℎ z
79 71 78 breqtrd ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A ∧ z ∈ B ∧ ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v ∧ norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
80 79 exp43 ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A → z ∈ B → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
81 80 com23 ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → z ∈ B → norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
82 81 ralrimdv ⊢ w ∈ ℝ ∧ 0 < w ∧ y ∈ A → ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
83 82 ralimdva ⊢ w ∈ ℝ ∧ 0 < w → ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
84 83 impr ⊢ w ∈ ℝ ∧ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
85 6 8 84 jca32 ⊢ w ∈ ℝ ∧ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → 1 w ∈ ℝ ∧ 0 < 1 w ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
86 85 ex ⊢ w ∈ ℝ → 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → 1 w ∈ ℝ ∧ 0 < 1 w ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
87 breq2 ⊢ x = 1 w → 0 < x ↔ 0 < 1 w
88 breq1 ⊢ x = 1 w → x ≤ norm ℎ ⁡ y - ℎ z ↔ 1 w ≤ norm ℎ ⁡ y - ℎ z
89 88 imbi2d ⊢ x = 1 w → norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z ↔ norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
90 89 2ralbidv ⊢ x = 1 w → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z ↔ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
91 87 90 anbi12d ⊢ x = 1 w → 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z ↔ 0 < 1 w ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z
92 91 rspcev ⊢ 1 w ∈ ℝ ∧ 0 < 1 w ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → 1 w ≤ norm ℎ ⁡ y - ℎ z → ∃ x ∈ ℝ 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z
93 86 92 syl6 ⊢ w ∈ ℝ → 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∃ x ∈ ℝ 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z
94 93 rexlimiv ⊢ ∃ w ∈ ℝ 0 < w ∧ ∀ y ∈ A ∀ v ∈ B norm ℎ ⁡ y + norm ℎ ⁡ v ≤ w ⁢ norm ℎ ⁡ y + ℎ v → ∃ x ∈ ℝ 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y = 1 → x ≤ norm ℎ ⁡ y - ℎ z