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 ⊢ A ∈ S ℋ
cdj3.2 ⊢ B ∈ S ℋ
cdj3.3 ⊢ S = x ∈ A + ℋ B ⟼ ι z ∈ A | ∃ w ∈ B x = z + ℎ w
cdj3.4 ⊢ T = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
cdj3.5 ⊢ φ ↔ ∃ v ∈ ℝ 0 < v ∧ ∀ u ∈ A + ℋ B norm ℎ ⁡ S ⁡ u ≤ v ⁢ norm ℎ ⁡ u
cdj3.6 ⊢ ψ ↔ ∃ v ∈ ℝ 0 < v ∧ ∀ u ∈ A + ℋ B norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u
Assertion cdj3i ⊢ ∃ v ∈ ℝ 0 < v ∧ ∀ x ∈ A ∀ y ∈ B norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ A ∩ B = 0 ℋ ∧ φ ∧ ψ

Proof

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