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

Proof

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