Metamath Proof Explorer

Theorem cdj3i

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

Ref Expression
Hypotheses cdj3.1 ⊢ 𝐴 ∈ Sℋ
cdj3.2 ⊢ 𝐵 ∈ Sℋ
cdj3.3 ⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
cdj3.4 ⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
cdj3.5 ⊢ ( 𝜑 ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
cdj3.6 ⊢ ( 𝜓 ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
Assertion cdj3i ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝜑 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 cdj3.1 ⊢ 𝐴 ∈ Sℋ
2 cdj3.2 ⊢ 𝐵 ∈ Sℋ
3 cdj3.3 ⊢ 𝑆 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
4 cdj3.4 ⊢ 𝑇 = ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↦ ( ℩ 𝑤 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑥 = ( 𝑧 +ℎ 𝑤 ) ) )
5 cdj3.5 ⊢ ( 𝜑 ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
6 cdj3.6 ⊢ ( 𝜓 ↔ ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
7 1 2 cdj3lem1 ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( 𝐴 ∩ 𝐵 ) = 0ℋ )
8 1 2 3 cdj3lem2b ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
9 8 5 sylibr ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → 𝜑 )
10 1 2 4 cdj3lem3b ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) )
11 10 6 sylibr ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → 𝜓 )
12 7 9 11 3jca ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝜑 ∧ 𝜓 ) )
13 breq2 ⊢ ( 𝑣 = 𝑓 → ( 0 < 𝑣 ↔ 0 < 𝑓 ) )
14 oveq1 ⊢ ( 𝑣 = 𝑓 → ( 𝑣 · ( normℎ ‘ 𝑢 ) ) = ( 𝑓 · ( normℎ ‘ 𝑢 ) ) )
15 14 breq2d ⊢ ( 𝑣 = 𝑓 → ( ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) )
16 15 ralbidv ⊢ ( 𝑣 = 𝑓 → ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) )
17 13 16 anbi12d ⊢ ( 𝑣 = 𝑓 → ( ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ) )
18 17 cbvrexvw ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ∃ 𝑓 ∈ ℝ ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) )
19 5 18 bitri ⊢ ( 𝜑 ↔ ∃ 𝑓 ∈ ℝ ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) )
20 breq2 ⊢ ( 𝑣 = 𝑔 → ( 0 < 𝑣 ↔ 0 < 𝑔 ) )
21 oveq1 ⊢ ( 𝑣 = 𝑔 → ( 𝑣 · ( normℎ ‘ 𝑢 ) ) = ( 𝑔 · ( normℎ ‘ 𝑢 ) ) )
22 21 breq2d ⊢ ( 𝑣 = 𝑔 → ( ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) )
23 22 ralbidv ⊢ ( 𝑣 = 𝑔 → ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) )
24 20 23 anbi12d ⊢ ( 𝑣 = 𝑔 → ( ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) )
25 24 cbvrexvw ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑣 · ( normℎ ‘ 𝑢 ) ) ) ↔ ∃ 𝑔 ∈ ℝ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) )
26 6 25 bitri ⊢ ( 𝜓 ↔ ∃ 𝑔 ∈ ℝ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) )
27 19 26 anbi12i ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑓 ∈ ℝ ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ∃ 𝑔 ∈ ℝ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) )
28 reeanv ⊢ ( ∃ 𝑓 ∈ ℝ ∃ 𝑔 ∈ ℝ ( ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) ↔ ( ∃ 𝑓 ∈ ℝ ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ∃ 𝑔 ∈ ℝ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) )
29 27 28 bitr4i ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑓 ∈ ℝ ∃ 𝑔 ∈ ℝ ( ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) )
30 an4 ⊢ ( ( ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) ↔ ( ( 0 < 𝑓 ∧ 0 < 𝑔 ) ∧ ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) )
31 addgt0 ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 0 < 𝑓 ∧ 0 < 𝑔 ) ) → 0 < ( 𝑓 + 𝑔 ) )
32 31 ex ⊢ ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) → ( ( 0 < 𝑓 ∧ 0 < 𝑔 ) → 0 < ( 𝑓 + 𝑔 ) ) )
33 32 adantl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) → ( ( 0 < 𝑓 ∧ 0 < 𝑔 ) → 0 < ( 𝑓 + 𝑔 ) ) )
34 1 2 shsvai ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑡 +ℎ ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) )
35 2fveq3 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) = ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) )
36 fveq2 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ 𝑢 ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
37 36 oveq2d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( 𝑓 · ( normℎ ‘ 𝑢 ) ) = ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
38 35 37 breq12d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
39 38 rspcv ⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) → ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
40 2fveq3 ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) = ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) )
41 36 oveq2d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( 𝑔 · ( normℎ ‘ 𝑢 ) ) = ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
42 40 41 breq12d ⊢ ( 𝑢 = ( 𝑡 +ℎ ℎ ) → ( ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ↔ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
43 42 rspcv ⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) → ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) → ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
44 39 43 anim12d ⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ( 𝐴 +ℋ 𝐵 ) → ( ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) → ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
45 34 44 syl ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) → ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
46 45 adantl ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) → ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
47 1 sheli ⊢ ( 𝑡 ∈ 𝐴 → 𝑡 ∈ ℋ )
48 normcl ⊢ ( 𝑡 ∈ ℋ → ( normℎ ‘ 𝑡 ) ∈ ℝ )
49 47 48 syl ⊢ ( 𝑡 ∈ 𝐴 → ( normℎ ‘ 𝑡 ) ∈ ℝ )
50 2 sheli ⊢ ( ℎ ∈ 𝐵 → ℎ ∈ ℋ )
51 normcl ⊢ ( ℎ ∈ ℋ → ( normℎ ‘ ℎ ) ∈ ℝ )
52 50 51 syl ⊢ ( ℎ ∈ 𝐵 → ( normℎ ‘ ℎ ) ∈ ℝ )
53 49 52 anim12i ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) )
54 53 adantl ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) )
55 hvaddcl ⊢ ( ( 𝑡 ∈ ℋ ∧ ℎ ∈ ℋ ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
56 47 50 55 syl2an ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( 𝑡 +ℎ ℎ ) ∈ ℋ )
57 normcl ⊢ ( ( 𝑡 +ℎ ℎ ) ∈ ℋ → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
58 56 57 syl ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ )
59 remulcl ⊢ ( ( 𝑓 ∈ ℝ ∧ ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ ) → ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
60 58 59 sylan2 ⊢ ( ( 𝑓 ∈ ℝ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
61 60 adantlr ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
62 remulcl ⊢ ( ( 𝑔 ∈ ℝ ∧ ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℝ ) → ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
63 58 62 sylan2 ⊢ ( ( 𝑔 ∈ ℝ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
64 63 adantll ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ )
65 le2add ⊢ ( ( ( ( normℎ ‘ 𝑡 ) ∈ ℝ ∧ ( normℎ ‘ ℎ ) ∈ ℝ ) ∧ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ ∧ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∈ ℝ ) ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
66 54 61 64 65 syl12anc ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
67 66 adantll ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
68 1 2 3 cdj3lem2 ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) = 𝑡 )
69 68 fveq2d ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ 𝑡 ) )
70 69 breq1d ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
71 1 2 4 cdj3lem3 ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) = ℎ )
72 71 fveq2d ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( normℎ ‘ ℎ ) )
73 72 breq1d ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
74 70 73 anbi12d ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
75 74 3expa ⊢ ( ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
76 75 ancoms ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
77 76 adantlr ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ℎ ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
78 recn ⊢ ( 𝑓 ∈ ℝ → 𝑓 ∈ ℂ )
79 recn ⊢ ( 𝑔 ∈ ℝ → 𝑔 ∈ ℂ )
80 58 recnd ⊢ ( ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) → ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℂ )
81 adddir ⊢ ( ( 𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ ∧ ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ∈ ℂ ) → ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
82 78 79 80 81 syl3an ⊢ ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
83 82 3expa ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
84 83 breq2d ⊢ ( ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
85 84 adantll ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) + ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
86 67 77 85 3imtr4d ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ( normℎ ‘ ( 𝑆 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑓 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ∧ ( normℎ ‘ ( 𝑇 ‘ ( 𝑡 +ℎ ℎ ) ) ) ≤ ( 𝑔 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
87 46 86 syld ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ) ) → ( ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
88 87 ralrimdvva ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) → ( ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) → ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
89 readdcl ⊢ ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) → ( 𝑓 + 𝑔 ) ∈ ℝ )
90 breq2 ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( 0 < 𝑣 ↔ 0 < ( 𝑓 + 𝑔 ) ) )
91 fveq2 ⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ 𝑥 ) = ( normℎ ‘ 𝑡 ) )
92 91 oveq1d ⊢ ( 𝑥 = 𝑡 → ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) )
93 fvoveq1 ⊢ ( 𝑥 = 𝑡 → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) )
94 93 oveq2d ⊢ ( 𝑥 = 𝑡 → ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) )
95 92 94 breq12d ⊢ ( 𝑥 = 𝑡 → ( ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ) )
96 fveq2 ⊢ ( 𝑦 = ℎ → ( normℎ ‘ 𝑦 ) = ( normℎ ‘ ℎ ) )
97 96 oveq2d ⊢ ( 𝑦 = ℎ → ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) = ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) )
98 oveq2 ⊢ ( 𝑦 = ℎ → ( 𝑡 +ℎ 𝑦 ) = ( 𝑡 +ℎ ℎ ) )
99 98 fveq2d ⊢ ( 𝑦 = ℎ → ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) = ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) )
100 99 oveq2d ⊢ ( 𝑦 = ℎ → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) = ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
101 97 100 breq12d ⊢ ( 𝑦 = ℎ → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ 𝑦 ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
102 95 101 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
103 oveq1 ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) = ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) )
104 103 breq2d ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
105 104 2ralbidv ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ↔ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
106 102 105 syl5bb ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ↔ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) )
107 90 106 anbi12d ⊢ ( 𝑣 = ( 𝑓 + 𝑔 ) → ( ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ↔ ( 0 < ( 𝑓 + 𝑔 ) ∧ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) )
108 107 rspcev ⊢ ( ( ( 𝑓 + 𝑔 ) ∈ ℝ ∧ ( 0 < ( 𝑓 + 𝑔 ) ∧ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) )
109 108 ex ⊢ ( ( 𝑓 + 𝑔 ) ∈ ℝ → ( ( 0 < ( 𝑓 + 𝑔 ) ∧ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
110 89 109 syl ⊢ ( ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) → ( ( 0 < ( 𝑓 + 𝑔 ) ∧ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
111 110 adantl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) → ( ( 0 < ( 𝑓 + 𝑔 ) ∧ ∀ 𝑡 ∈ 𝐴 ∀ ℎ ∈ 𝐵 ( ( normℎ ‘ 𝑡 ) + ( normℎ ‘ ℎ ) ) ≤ ( ( 𝑓 + 𝑔 ) · ( normℎ ‘ ( 𝑡 +ℎ ℎ ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
112 33 88 111 syl2and ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) → ( ( ( 0 < 𝑓 ∧ 0 < 𝑔 ) ∧ ( ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
113 30 112 syl5bi ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ ( 𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ) ) → ( ( ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
114 113 rexlimdvva ⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ∃ 𝑓 ∈ ℝ ∃ 𝑔 ∈ ℝ ( ( 0 < 𝑓 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑆 ‘ 𝑢 ) ) ≤ ( 𝑓 · ( normℎ ‘ 𝑢 ) ) ) ∧ ( 0 < 𝑔 ∧ ∀ 𝑢 ∈ ( 𝐴 +ℋ 𝐵 ) ( normℎ ‘ ( 𝑇 ‘ 𝑢 ) ) ≤ ( 𝑔 · ( normℎ ‘ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
115 29 114 syl5bi ⊢ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ) )
116 115 3impib ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝜑 ∧ 𝜓 ) → ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) )
117 12 116 impbii ⊢ ( ∃ 𝑣 ∈ ℝ ( 0 < 𝑣 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) ≤ ( 𝑣 · ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝜑 ∧ 𝜓 ) )