Metamath Proof Explorer

Theorem cdj3lem1

Description: A property of " A and B are completely disjoint subspaces." Part of Lemma 5 of Holland p. 1520. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cdj1.1 ⊢ A ∈ S ℋ
2 cdj1.2 ⊢ B ∈ S ℋ
3 elin ⊢ w ∈ A ∩ B ↔ w ∈ A ∧ w ∈ B
4 neg1cn ⊢ − 1 ∈ ℂ
5 shmulcl ⊢ B ∈ S ℋ ∧ − 1 ∈ ℂ ∧ w ∈ B → -1 ⋅ ℎ w ∈ B
6 2 4 5 mp3an12 ⊢ w ∈ B → -1 ⋅ ℎ w ∈ B
7 6 anim2i ⊢ w ∈ A ∧ w ∈ B → w ∈ A ∧ -1 ⋅ ℎ w ∈ B
8 3 7 sylbi ⊢ w ∈ A ∩ B → w ∈ A ∧ -1 ⋅ ℎ w ∈ B
9 fveq2 ⊢ y = w → norm ℎ ⁡ y = norm ℎ ⁡ w
10 9 oveq1d ⊢ y = w → norm ℎ ⁡ y + norm ℎ ⁡ z = norm ℎ ⁡ w + norm ℎ ⁡ z
11 fvoveq1 ⊢ y = w → norm ℎ ⁡ y + ℎ z = norm ℎ ⁡ w + ℎ z
12 11 oveq2d ⊢ y = w → x ⁢ norm ℎ ⁡ y + ℎ z = x ⁢ norm ℎ ⁡ w + ℎ z
13 10 12 breq12d ⊢ y = w → norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z ↔ norm ℎ ⁡ w + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ w + ℎ z
14 fveq2 ⊢ z = -1 ⋅ ℎ w → norm ℎ ⁡ z = norm ℎ ⁡ -1 ⋅ ℎ w
15 14 oveq2d ⊢ z = -1 ⋅ ℎ w → norm ℎ ⁡ w + norm ℎ ⁡ z = norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w
16 oveq2 ⊢ z = -1 ⋅ ℎ w → w + ℎ z = w + ℎ -1 ⋅ ℎ w
17 16 fveq2d ⊢ z = -1 ⋅ ℎ w → norm ℎ ⁡ w + ℎ z = norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
18 17 oveq2d ⊢ z = -1 ⋅ ℎ w → x ⁢ norm ℎ ⁡ w + ℎ z = x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
19 15 18 breq12d ⊢ z = -1 ⋅ ℎ w → norm ℎ ⁡ w + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ w + ℎ z ↔ norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
20 13 19 rspc2v ⊢ w ∈ A ∧ -1 ⋅ ℎ w ∈ B → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
21 8 20 syl ⊢ w ∈ A ∩ B → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
22 21 adantl ⊢ x ∈ ℝ ∧ w ∈ A ∩ B → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w
23 1 2 shincli ⊢ A ∩ B ∈ S ℋ
24 23 sheli ⊢ w ∈ A ∩ B → w ∈ ℋ
25 normneg ⊢ w ∈ ℋ → norm ℎ ⁡ -1 ⋅ ℎ w = norm ℎ ⁡ w
26 25 oveq2d ⊢ w ∈ ℋ → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w = norm ℎ ⁡ w + norm ℎ ⁡ w
27 normcl ⊢ w ∈ ℋ → norm ℎ ⁡ w ∈ ℝ
28 27 recnd ⊢ w ∈ ℋ → norm ℎ ⁡ w ∈ ℂ
29 28 2timesd ⊢ w ∈ ℋ → 2 ⁢ norm ℎ ⁡ w = norm ℎ ⁡ w + norm ℎ ⁡ w
30 26 29 eqtr4d ⊢ w ∈ ℋ → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w = 2 ⁢ norm ℎ ⁡ w
31 30 adantl ⊢ x ∈ ℝ ∧ w ∈ ℋ → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w = 2 ⁢ norm ℎ ⁡ w
32 hvnegid ⊢ w ∈ ℋ → w + ℎ -1 ⋅ ℎ w = 0 ℎ
33 32 fveq2d ⊢ w ∈ ℋ → norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w = norm ℎ ⁡ 0 ℎ
34 norm0 ⊢ norm ℎ ⁡ 0 ℎ = 0
35 33 34 eqtrdi ⊢ w ∈ ℋ → norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w = 0
36 35 oveq2d ⊢ w ∈ ℋ → x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w = x ⋅ 0
37 recn ⊢ x ∈ ℝ → x ∈ ℂ
38 37 mul01d ⊢ x ∈ ℝ → x ⋅ 0 = 0
39 36 38 sylan9eqr ⊢ x ∈ ℝ ∧ w ∈ ℋ → x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w = 0
40 2t0e0 ⊢ 2 ⋅ 0 = 0
41 39 40 eqtr4di ⊢ x ∈ ℝ ∧ w ∈ ℋ → x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w = 2 ⋅ 0
42 31 41 breq12d ⊢ x ∈ ℝ ∧ w ∈ ℋ → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w ↔ 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0
43 0re ⊢ 0 ∈ ℝ
44 letri3 ⊢ norm ℎ ⁡ w ∈ ℝ ∧ 0 ∈ ℝ → norm ℎ ⁡ w = 0 ↔ norm ℎ ⁡ w ≤ 0 ∧ 0 ≤ norm ℎ ⁡ w
45 27 43 44 sylancl ⊢ w ∈ ℋ → norm ℎ ⁡ w = 0 ↔ norm ℎ ⁡ w ≤ 0 ∧ 0 ≤ norm ℎ ⁡ w
46 normge0 ⊢ w ∈ ℋ → 0 ≤ norm ℎ ⁡ w
47 46 biantrud ⊢ w ∈ ℋ → norm ℎ ⁡ w ≤ 0 ↔ norm ℎ ⁡ w ≤ 0 ∧ 0 ≤ norm ℎ ⁡ w
48 2re ⊢ 2 ∈ ℝ
49 2pos ⊢ 0 < 2
50 48 49 pm3.2i ⊢ 2 ∈ ℝ ∧ 0 < 2
51 lemul2 ⊢ norm ℎ ⁡ w ∈ ℝ ∧ 0 ∈ ℝ ∧ 2 ∈ ℝ ∧ 0 < 2 → norm ℎ ⁡ w ≤ 0 ↔ 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0
52 43 50 51 mp3an23 ⊢ norm ℎ ⁡ w ∈ ℝ → norm ℎ ⁡ w ≤ 0 ↔ 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0
53 27 52 syl ⊢ w ∈ ℋ → norm ℎ ⁡ w ≤ 0 ↔ 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0
54 45 47 53 3bitr2rd ⊢ w ∈ ℋ → 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0 ↔ norm ℎ ⁡ w = 0
55 norm-i ⊢ w ∈ ℋ → norm ℎ ⁡ w = 0 ↔ w = 0 ℎ
56 54 55 bitrd ⊢ w ∈ ℋ → 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0 ↔ w = 0 ℎ
57 56 adantl ⊢ x ∈ ℝ ∧ w ∈ ℋ → 2 ⁢ norm ℎ ⁡ w ≤ 2 ⋅ 0 ↔ w = 0 ℎ
58 42 57 bitrd ⊢ x ∈ ℝ ∧ w ∈ ℋ → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w ↔ w = 0 ℎ
59 24 58 sylan2 ⊢ x ∈ ℝ ∧ w ∈ A ∩ B → norm ℎ ⁡ w + norm ℎ ⁡ -1 ⋅ ℎ w ≤ x ⁢ norm ℎ ⁡ w + ℎ -1 ⋅ ℎ w ↔ w = 0 ℎ
60 22 59 sylibd ⊢ x ∈ ℝ ∧ w ∈ A ∩ B → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → w = 0 ℎ
61 60 impancom ⊢ x ∈ ℝ ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → w ∈ A ∩ B → w = 0 ℎ
62 elch0 ⊢ w ∈ 0 ℋ ↔ w = 0 ℎ
63 61 62 syl6ibr ⊢ x ∈ ℝ ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → w ∈ A ∩ B → w ∈ 0 ℋ
64 63 ssrdv ⊢ x ∈ ℝ ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → A ∩ B ⊆ 0 ℋ
65 64 ex ⊢ x ∈ ℝ → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → A ∩ B ⊆ 0 ℋ
66 shle0 ⊢ A ∩ B ∈ S ℋ → A ∩ B ⊆ 0 ℋ ↔ A ∩ B = 0 ℋ
67 23 66 ax-mp ⊢ A ∩ B ⊆ 0 ℋ ↔ A ∩ B = 0 ℋ
68 65 67 syl6ib ⊢ x ∈ ℝ → ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → A ∩ B = 0 ℋ
69 68 adantld ⊢ x ∈ ℝ → 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → A ∩ B = 0 ℋ
70 69 rexlimiv ⊢ ∃ x ∈ ℝ 0 < x ∧ ∀ y ∈ A ∀ z ∈ B norm ℎ ⁡ y + norm ℎ ⁡ z ≤ x ⁢ norm ℎ ⁡ y + ℎ z → A ∩ B = 0 ℋ