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 ⊢ 𝐴 ∈ Sℋ
cdj1.2 ⊢ 𝐵 ∈ Sℋ
Assertion cdj3lem1 ( ∃ 𝑥 ∈ ℝ ( 0 < 𝑥 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( ( normℎ ‘ 𝑦 ) + ( normℎ ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ ( 𝑦 +ℎ 𝑧 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )

Proof

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