Metamath Proof Explorer

Theorem cdj3lem2b

Description: Lemma for cdj3i . The first-component function S is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005) (New usage is discouraged.)

Ref Expression
Hypotheses cdj3lem2.1 ⊢ 𝐴 ∈ Sℋ
cdj3lem2.2 ⊢ 𝐵 ∈ Sℋ
cdj3lem2.3 ⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
Assertion cdj3lem2b ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢ 𝐴 ∈ Sℋ
2 cdj3lem2.2 ⊢ 𝐵 ∈ Sℋ
3 cdj3lem2.3 ⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4 1 2 cdj3lem1 ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )
5 1 2 shseli ⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) )
6 5 biimpi ⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) )
7 fveq2 ⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝑡 ) )
8 7 oveq1d ⊢ ( 𝑥 = 𝑡 → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) )
9 fvoveq1 ⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) )
10 9 oveq2d ⊢ ( 𝑥 = 𝑡 → ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) )
11 8 10 breq12d ⊢ ( 𝑥 = 𝑡 → ( ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ) )
12 fveq2 ⊢ ( 𝑦 = ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ ℎ ) )
13 12 oveq2d ⊢ ( 𝑦 = ℎ → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
14 oveq2 ⊢ ( 𝑦 = ℎ → ( 𝑡 +ℎ 𝑦 ) = ( 𝑡 +ℎ ℎ ) )
15 14 fveq2d ⊢ ( 𝑦 = ℎ → ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
16 15 oveq2d ⊢ ( 𝑦 = ℎ → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
17 13 16 breq12d ⊢ ( 𝑦 = ℎ → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
18 11 17 rspc2v ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
19 1 2 3 cdj3lem2 ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) = 𝑡 )
20 19 3expa ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) = 𝑡 )
21 20 fveq2d ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ 𝑡 ) )
22 21 ad2ant2r ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ 𝑡 ) )
23 2 sheli ⊢ ( ℎ ∈ 𝐵 → ℎ ∈ ℋ )
24 normge0 ⊢ ( ℎ ∈ ℋ → 0 ≤ ( normℎ ‘ ℎ ) )
25 23 24 syl ⊢ ( ℎ ∈ 𝐵 → 0 ≤ ( normℎ ‘ ℎ ) )
26 25 adantl ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → 0 ≤ ( normℎ ‘ ℎ ) )
27 1 sheli ⊢ ( 𝑡 ∈ 𝐴 → 𝑡 ∈ ℋ )
28 normcl ⊢ ( 𝑡 ∈ ℋ → ( normℎ ‘ 𝑡 ) ∈ ℝ )
29 27 28 syl ⊢ ( 𝑡 ∈ 𝐴 → ( normℎ ‘ 𝑡 ) ∈ ℝ )
30 normcl ⊢ ( ℎ ∈ ℋ → ( normℎ ‘ ℎ ) ∈ ℝ )
31 23 30 syl ⊢ ( ℎ ∈ 𝐵 → ( normℎ ‘ ℎ ) ∈ ℝ )
32 addge01 ⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) → ( 0 ≤ ( normℎ ‘ ℎ ) ↔ ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ) )
33 29 31 32 syl2an ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 0 ≤ ( normℎ ‘ ℎ ) ↔ ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ) )
34 26 33 mpbid ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
35 34 adantr ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
36 29 ad2antrr ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ∈ ℝ )
37 readdcl ⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
38 29 31 37 syl2an ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
39 38 adantr ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ )
40 hvaddcl ⊢ ( ( 𝑡 ∈ ℋ ∧ ℎ ∈ ℋ ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
41 27 23 40 syl2an ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
42 normcl ⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ℋ → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
43 41 42 syl ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
44 remulcl ⊢ ( ( 𝑣 ∈ ℝ ∧ ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
45 43 44 sylan2 ⊢ ( ( 𝑣 ∈ ℝ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
46 45 ancoms ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
47 letr ⊢ ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∈ ℝ ∧ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
48 36 39 46 47 syl3anc ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
49 35 48 mpand ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
50 49 imp ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ 𝑣 ∈ ℝ ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
51 50 an32s ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ 𝑣 ∈ ℝ ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
52 51 adantrl ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ 𝑡 ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
53 22 52 eqbrtrd ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
54 2fveq3 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) )
55 fveq2 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ 𝑢 ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
56 55 oveq2d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( 𝑣 · ( normℎ ‘ 𝑢 ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
57 54 56 breq12d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
58 53 57 syl5ibrcom ⊢ ( ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ∧ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
59 58 exp31 ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
60 18 59 syld ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
61 60 com14 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
62 61 com4t ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) ) )
63 62 rexlimdvv ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∃ 𝑡 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
64 6 63 syl5com ⊢ ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
65 64 com3l ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ( 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
66 65 ralrimdv ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) → ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
67 66 anim2d ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝑣 ∈ ℝ ) → ( ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
68 67 reximdva ⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ) )
69 4 68 mpcom ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )