Metamath Proof Explorer

Theorem cdj3lem3b

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

Ref Expression
Hypotheses cdj3lem2.1 ⊢ A ∈ S ℋ
cdj3lem2.2 ⊢ B ∈ S ℋ
cdj3lem3.3 ⊢ T = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
Assertion 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

Proof

Step Hyp Ref Expression
1 cdj3lem2.1 ⊢ A ∈ S ℋ
2 cdj3lem2.2 ⊢ B ∈ S ℋ
3 cdj3lem3.3 ⊢ T = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
4 2 1 shscomi ⊢ B + ℋ A = A + ℋ B
5 2 sheli ⊢ w ∈ B → w ∈ ℋ
6 1 sheli ⊢ z ∈ A → z ∈ ℋ
7 ax-hvcom ⊢ w ∈ ℋ ∧ z ∈ ℋ → w + ℎ z = z + ℎ w
8 5 6 7 syl2an ⊢ w ∈ B ∧ z ∈ A → w + ℎ z = z + ℎ w
9 8 eqeq2d ⊢ w ∈ B ∧ z ∈ A → x = w + ℎ z ↔ x = z + ℎ w
10 9 rexbidva ⊢ w ∈ B → ∃ z ∈ A x = w + ℎ z ↔ ∃ z ∈ A x = z + ℎ w
11 10 riotabiia ⊢ ι w ∈ B | ∃ z ∈ A x = w + ℎ z = ι w ∈ B | ∃ z ∈ A x = z + ℎ w
12 4 11 mpteq12i ⊢ x ∈ B + ℋ A ⟼ ι w ∈ B | ∃ z ∈ A x = w + ℎ z = x ∈ A + ℋ B ⟼ ι w ∈ B | ∃ z ∈ A x = z + ℎ w
13 3 12 eqtr4i ⊢ T = x ∈ B + ℋ A ⟼ ι w ∈ B | ∃ z ∈ A x = w + ℎ z
14 2 1 13 cdj3lem2b ⊢ ∃ v ∈ ℝ 0 < v ∧ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y → ∃ v ∈ ℝ 0 < v ∧ ∀ u ∈ B + ℋ A norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u
15 fveq2 ⊢ x = t → norm ℎ ⁡ x = norm ℎ ⁡ t
16 15 oveq1d ⊢ x = t → norm ℎ ⁡ x + norm ℎ ⁡ y = norm ℎ ⁡ t + norm ℎ ⁡ y
17 fvoveq1 ⊢ x = t → norm ℎ ⁡ x + ℎ y = norm ℎ ⁡ t + ℎ y
18 17 oveq2d ⊢ x = t → v ⁢ norm ℎ ⁡ x + ℎ y = v ⁢ norm ℎ ⁡ t + ℎ y
19 16 18 breq12d ⊢ x = t → norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ norm ℎ ⁡ t + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ t + ℎ y
20 fveq2 ⊢ y = h → norm ℎ ⁡ y = norm ℎ ⁡ h
21 20 oveq2d ⊢ y = h → norm ℎ ⁡ t + norm ℎ ⁡ y = norm ℎ ⁡ t + norm ℎ ⁡ h
22 oveq2 ⊢ y = h → t + ℎ y = t + ℎ h
23 22 fveq2d ⊢ y = h → norm ℎ ⁡ t + ℎ y = norm ℎ ⁡ t + ℎ h
24 23 oveq2d ⊢ y = h → v ⁢ norm ℎ ⁡ t + ℎ y = v ⁢ norm ℎ ⁡ t + ℎ h
25 21 24 breq12d ⊢ y = h → norm ℎ ⁡ t + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ t + ℎ y ↔ norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h
26 19 25 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
27 ralcom ⊢ ∀ t ∈ A ∀ h ∈ B norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h ↔ ∀ h ∈ B ∀ t ∈ A norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h
28 2 sheli ⊢ x ∈ B → x ∈ ℋ
29 normcl ⊢ x ∈ ℋ → norm ℎ ⁡ x ∈ ℝ
30 28 29 syl ⊢ x ∈ B → norm ℎ ⁡ x ∈ ℝ
31 30 recnd ⊢ x ∈ B → norm ℎ ⁡ x ∈ ℂ
32 1 sheli ⊢ y ∈ A → y ∈ ℋ
33 normcl ⊢ y ∈ ℋ → norm ℎ ⁡ y ∈ ℝ
34 32 33 syl ⊢ y ∈ A → norm ℎ ⁡ y ∈ ℝ
35 34 recnd ⊢ y ∈ A → norm ℎ ⁡ y ∈ ℂ
36 addcom ⊢ norm ℎ ⁡ x ∈ ℂ ∧ norm ℎ ⁡ y ∈ ℂ → norm ℎ ⁡ x + norm ℎ ⁡ y = norm ℎ ⁡ y + norm ℎ ⁡ x
37 31 35 36 syl2an ⊢ x ∈ B ∧ y ∈ A → norm ℎ ⁡ x + norm ℎ ⁡ y = norm ℎ ⁡ y + norm ℎ ⁡ x
38 ax-hvcom ⊢ x ∈ ℋ ∧ y ∈ ℋ → x + ℎ y = y + ℎ x
39 28 32 38 syl2an ⊢ x ∈ B ∧ y ∈ A → x + ℎ y = y + ℎ x
40 39 fveq2d ⊢ x ∈ B ∧ y ∈ A → norm ℎ ⁡ x + ℎ y = norm ℎ ⁡ y + ℎ x
41 40 oveq2d ⊢ x ∈ B ∧ y ∈ A → v ⁢ norm ℎ ⁡ x + ℎ y = v ⁢ norm ℎ ⁡ y + ℎ x
42 37 41 breq12d ⊢ x ∈ B ∧ y ∈ A → norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ norm ℎ ⁡ y + norm ℎ ⁡ x ≤ v ⁢ norm ℎ ⁡ y + ℎ x
43 42 ralbidva ⊢ x ∈ B → ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ ∀ y ∈ A norm ℎ ⁡ y + norm ℎ ⁡ x ≤ v ⁢ norm ℎ ⁡ y + ℎ x
44 43 ralbiia ⊢ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ y + norm ℎ ⁡ x ≤ v ⁢ norm ℎ ⁡ y + ℎ x
45 fveq2 ⊢ x = h → norm ℎ ⁡ x = norm ℎ ⁡ h
46 45 oveq2d ⊢ x = h → norm ℎ ⁡ y + norm ℎ ⁡ x = norm ℎ ⁡ y + norm ℎ ⁡ h
47 oveq2 ⊢ x = h → y + ℎ x = y + ℎ h
48 47 fveq2d ⊢ x = h → norm ℎ ⁡ y + ℎ x = norm ℎ ⁡ y + ℎ h
49 48 oveq2d ⊢ x = h → v ⁢ norm ℎ ⁡ y + ℎ x = v ⁢ norm ℎ ⁡ y + ℎ h
50 46 49 breq12d ⊢ x = h → norm ℎ ⁡ y + norm ℎ ⁡ x ≤ v ⁢ norm ℎ ⁡ y + ℎ x ↔ norm ℎ ⁡ y + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ y + ℎ h
51 fveq2 ⊢ y = t → norm ℎ ⁡ y = norm ℎ ⁡ t
52 51 oveq1d ⊢ y = t → norm ℎ ⁡ y + norm ℎ ⁡ h = norm ℎ ⁡ t + norm ℎ ⁡ h
53 fvoveq1 ⊢ y = t → norm ℎ ⁡ y + ℎ h = norm ℎ ⁡ t + ℎ h
54 53 oveq2d ⊢ y = t → v ⁢ norm ℎ ⁡ y + ℎ h = v ⁢ norm ℎ ⁡ t + ℎ h
55 52 54 breq12d ⊢ y = t → norm ℎ ⁡ y + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ y + ℎ h ↔ norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h
56 50 55 cbvral2vw ⊢ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ y + norm ℎ ⁡ x ≤ v ⁢ norm ℎ ⁡ y + ℎ x ↔ ∀ h ∈ B ∀ t ∈ A norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h
57 44 56 bitr2i ⊢ ∀ h ∈ B ∀ t ∈ A norm ℎ ⁡ t + norm ℎ ⁡ h ≤ v ⁢ norm ℎ ⁡ t + ℎ h ↔ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y
58 26 27 57 3bitri ⊢ ∀ x ∈ A ∀ y ∈ B norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y
59 58 anbi2i ⊢ 0 < v ∧ ∀ x ∈ A ∀ y ∈ B norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ 0 < v ∧ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y
60 59 rexbii ⊢ ∃ v ∈ ℝ 0 < v ∧ ∀ x ∈ A ∀ y ∈ B norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y ↔ ∃ v ∈ ℝ 0 < v ∧ ∀ x ∈ B ∀ y ∈ A norm ℎ ⁡ x + norm ℎ ⁡ y ≤ v ⁢ norm ℎ ⁡ x + ℎ y
61 1 2 shscomi ⊢ A + ℋ B = B + ℋ A
62 61 raleqi ⊢ ∀ u ∈ A + ℋ B norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u ↔ ∀ u ∈ B + ℋ A norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u
63 62 anbi2i ⊢ 0 < v ∧ ∀ u ∈ A + ℋ B norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u ↔ 0 < v ∧ ∀ u ∈ B + ℋ A norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u
64 63 rexbii ⊢ ∃ v ∈ ℝ 0 < v ∧ ∀ u ∈ A + ℋ B norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u ↔ ∃ v ∈ ℝ 0 < v ∧ ∀ u ∈ B + ℋ A norm ℎ ⁡ T ⁡ u ≤ v ⁢ norm ℎ ⁡ u
65 14 60 64 3imtr4i ⊢ ∃ 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