HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  cdj3i Structured version   Visualization version   GIF version

Theorem cdj3i 28466
Description: Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdj3.1 𝐴S
cdj3.2 𝐵S
cdj3.3 𝑆 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑧𝐴𝑤𝐵 𝑥 = (𝑧 + 𝑤)))
cdj3.4 𝑇 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
cdj3.5 (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))))
cdj3.6 (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))))
Assertion
Ref Expression
cdj3i (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) ↔ ((𝐴𝐵) = 0𝜑𝜓))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝐴   𝑥,𝐵,𝑦,𝑧,𝑤,𝑣,𝑢   𝑣,𝑆,𝑢   𝑣,𝑇,𝑢
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝜓(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝑆(𝑥,𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem cdj3i
Dummy variables 𝑡 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cdj3.1 . . . 4 𝐴S
2 cdj3.2 . . . 4 𝐵S
31, 2cdj3lem1 28459 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → (𝐴𝐵) = 0)
4 cdj3.3 . . . . 5 𝑆 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑧𝐴𝑤𝐵 𝑥 = (𝑧 + 𝑤)))
51, 2, 4cdj3lem2b 28462 . . . 4 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))))
6 cdj3.5 . . . 4 (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))))
75, 6sylibr 222 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → 𝜑)
8 cdj3.4 . . . . 5 𝑇 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
91, 2, 8cdj3lem3b 28465 . . . 4 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))))
10 cdj3.6 . . . 4 (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))))
119, 10sylibr 222 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → 𝜓)
123, 7, 113jca 1234 . 2 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ((𝐴𝐵) = 0𝜑𝜓))
13 breq2 4485 . . . . . . . . 9 (𝑣 = 𝑓 → (0 < 𝑣 ↔ 0 < 𝑓))
14 oveq1 6438 . . . . . . . . . . 11 (𝑣 = 𝑓 → (𝑣 · (norm𝑢)) = (𝑓 · (norm𝑢)))
1514breq2d 4493 . . . . . . . . . 10 (𝑣 = 𝑓 → ((norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ (norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
1615ralbidv 2873 . . . . . . . . 9 (𝑣 = 𝑓 → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
1713, 16anbi12d 742 . . . . . . . 8 (𝑣 = 𝑓 → ((0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)))))
1817cbvrexv 3052 . . . . . . 7 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ ∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
196, 18bitri 262 . . . . . 6 (𝜑 ↔ ∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
20 breq2 4485 . . . . . . . . 9 (𝑣 = 𝑔 → (0 < 𝑣 ↔ 0 < 𝑔))
21 oveq1 6438 . . . . . . . . . . 11 (𝑣 = 𝑔 → (𝑣 · (norm𝑢)) = (𝑔 · (norm𝑢)))
2221breq2d 4493 . . . . . . . . . 10 (𝑣 = 𝑔 → ((norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ (norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2322ralbidv 2873 . . . . . . . . 9 (𝑣 = 𝑔 → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2420, 23anbi12d 742 . . . . . . . 8 (𝑣 = 𝑔 → ((0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
2524cbvrexv 3052 . . . . . . 7 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2610, 25bitri 262 . . . . . 6 (𝜓 ↔ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2719, 26anbi12i 728 . . . . 5 ((𝜑𝜓) ↔ (∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
28 reeanv 2990 . . . . 5 (∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) ↔ (∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
2927, 28bitr4i 265 . . . 4 ((𝜑𝜓) ↔ ∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
30 an4 860 . . . . . 6 (((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) ↔ ((0 < 𝑓 ∧ 0 < 𝑔) ∧ (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
31 addgt0 10266 . . . . . . . . 9 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (0 < 𝑓 ∧ 0 < 𝑔)) → 0 < (𝑓 + 𝑔))
3231ex 448 . . . . . . . 8 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → ((0 < 𝑓 ∧ 0 < 𝑔) → 0 < (𝑓 + 𝑔)))
3332adantl 480 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((0 < 𝑓 ∧ 0 < 𝑔) → 0 < (𝑓 + 𝑔)))
341, 2shsvai 27389 . . . . . . . . . . 11 ((𝑡𝐴𝐵) → (𝑡 + ) ∈ (𝐴 + 𝐵))
35 fveq2 5992 . . . . . . . . . . . . . . 15 (𝑢 = (𝑡 + ) → (𝑆𝑢) = (𝑆‘(𝑡 + )))
3635fveq2d 5996 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (norm‘(𝑆𝑢)) = (norm‘(𝑆‘(𝑡 + ))))
37 fveq2 5992 . . . . . . . . . . . . . . 15 (𝑢 = (𝑡 + ) → (norm𝑢) = (norm‘(𝑡 + )))
3837oveq2d 6447 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (𝑓 · (norm𝑢)) = (𝑓 · (norm‘(𝑡 + ))))
3936, 38breq12d 4494 . . . . . . . . . . . . 13 (𝑢 = (𝑡 + ) → ((norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ↔ (norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + )))))
4039rspcv 3182 . . . . . . . . . . . 12 ((𝑡 + ) ∈ (𝐴 + 𝐵) → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) → (norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + )))))
41 fveq2 5992 . . . . . . . . . . . . . . 15 (𝑢 = (𝑡 + ) → (𝑇𝑢) = (𝑇‘(𝑡 + )))
4241fveq2d 5996 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (norm‘(𝑇𝑢)) = (norm‘(𝑇‘(𝑡 + ))))
4337oveq2d 6447 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (𝑔 · (norm𝑢)) = (𝑔 · (norm‘(𝑡 + ))))
4442, 43breq12d 4494 . . . . . . . . . . . . 13 (𝑢 = (𝑡 + ) → ((norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)) ↔ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))))
4544rspcv 3182 . . . . . . . . . . . 12 ((𝑡 + ) ∈ (𝐴 + 𝐵) → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)) → (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))))
4640, 45anim12d 583 . . . . . . . . . . 11 ((𝑡 + ) ∈ (𝐴 + 𝐵) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
4734, 46syl 17 . . . . . . . . . 10 ((𝑡𝐴𝐵) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
4847adantl 480 . . . . . . . . 9 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
491sheli 27237 . . . . . . . . . . . . . . 15 (𝑡𝐴𝑡 ∈ ℋ)
50 normcl 27148 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℋ → (norm𝑡) ∈ ℝ)
5149, 50syl 17 . . . . . . . . . . . . . 14 (𝑡𝐴 → (norm𝑡) ∈ ℝ)
522sheli 27237 . . . . . . . . . . . . . . 15 (𝐵 ∈ ℋ)
53 normcl 27148 . . . . . . . . . . . . . . 15 ( ∈ ℋ → (norm) ∈ ℝ)
5452, 53syl 17 . . . . . . . . . . . . . 14 (𝐵 → (norm) ∈ ℝ)
5551, 54anim12i 587 . . . . . . . . . . . . 13 ((𝑡𝐴𝐵) → ((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ))
5655adantl 480 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → ((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ))
57 hvaddcl 27035 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℋ ∧ ∈ ℋ) → (𝑡 + ) ∈ ℋ)
5849, 52, 57syl2an 492 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵) → (𝑡 + ) ∈ ℋ)
59 normcl 27148 . . . . . . . . . . . . . . 15 ((𝑡 + ) ∈ ℋ → (norm‘(𝑡 + )) ∈ ℝ)
6058, 59syl 17 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵) → (norm‘(𝑡 + )) ∈ ℝ)
61 remulcl 9780 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℝ ∧ (norm‘(𝑡 + )) ∈ ℝ) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
6260, 61sylan2 489 . . . . . . . . . . . . 13 ((𝑓 ∈ ℝ ∧ (𝑡𝐴𝐵)) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
6362adantlr 746 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
64 remulcl 9780 . . . . . . . . . . . . . 14 ((𝑔 ∈ ℝ ∧ (norm‘(𝑡 + )) ∈ ℝ) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
6560, 64sylan2 489 . . . . . . . . . . . . 13 ((𝑔 ∈ ℝ ∧ (𝑡𝐴𝐵)) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
6665adantll 745 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
67 le2add 10262 . . . . . . . . . . . 12 ((((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ) ∧ ((𝑓 · (norm‘(𝑡 + ))) ∈ ℝ ∧ (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
6856, 63, 66, 67syl12anc 1315 . . . . . . . . . . 11 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
6968adantll 745 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
701, 2, 4cdj3lem2 28460 . . . . . . . . . . . . . . . 16 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (𝑆‘(𝑡 + )) = 𝑡)
7170fveq2d 5996 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (norm‘(𝑆‘(𝑡 + ))) = (norm𝑡))
7271breq1d 4491 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ↔ (norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + )))))
731, 2, 8cdj3lem3 28463 . . . . . . . . . . . . . . . 16 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (𝑇‘(𝑡 + )) = )
7473fveq2d 5996 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (norm‘(𝑇‘(𝑡 + ))) = (norm))
7574breq1d 4491 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → ((norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))) ↔ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))))
7672, 75anbi12d 742 . . . . . . . . . . . . 13 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
77763expa 1256 . . . . . . . . . . . 12 (((𝑡𝐴𝐵) ∧ (𝐴𝐵) = 0) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
7877ancoms 467 . . . . . . . . . . 11 (((𝐴𝐵) = 0 ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
7978adantlr 746 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
80 recn 9785 . . . . . . . . . . . . . 14 (𝑓 ∈ ℝ → 𝑓 ∈ ℂ)
81 recn 9785 . . . . . . . . . . . . . 14 (𝑔 ∈ ℝ → 𝑔 ∈ ℂ)
8260recnd 9827 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵) → (norm‘(𝑡 + )) ∈ ℂ)
83 adddir 9790 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ ∧ (norm‘(𝑡 + )) ∈ ℂ) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
8480, 81, 82, 83syl3an 1359 . . . . . . . . . . . . 13 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ∧ (𝑡𝐴𝐵)) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
85843expa 1256 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
8685breq2d 4493 . . . . . . . . . . 11 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
8786adantll 745 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
8869, 79, 873imtr4d 281 . . . . . . . . 9 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
8948, 88syld 45 . . . . . . . 8 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
9089ralrimdvva 2861 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
91 readdcl 9778 . . . . . . . . 9 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 + 𝑔) ∈ ℝ)
92 breq2 4485 . . . . . . . . . . . 12 (𝑣 = (𝑓 + 𝑔) → (0 < 𝑣 ↔ 0 < (𝑓 + 𝑔)))
93 fveq2 5992 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (norm𝑥) = (norm𝑡))
9493oveq1d 6446 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → ((norm𝑥) + (norm𝑦)) = ((norm𝑡) + (norm𝑦)))
95 oveq1 6438 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑡 → (𝑥 + 𝑦) = (𝑡 + 𝑦))
9695fveq2d 5996 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (norm‘(𝑥 + 𝑦)) = (norm‘(𝑡 + 𝑦)))
9796oveq2d 6447 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → (𝑣 · (norm‘(𝑥 + 𝑦))) = (𝑣 · (norm‘(𝑡 + 𝑦))))
9894, 97breq12d 4494 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ((norm𝑡) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑡 + 𝑦)))))
99 fveq2 5992 . . . . . . . . . . . . . . . 16 (𝑦 = → (norm𝑦) = (norm))
10099oveq2d 6447 . . . . . . . . . . . . . . 15 (𝑦 = → ((norm𝑡) + (norm𝑦)) = ((norm𝑡) + (norm)))
101 oveq2 6439 . . . . . . . . . . . . . . . . 17 (𝑦 = → (𝑡 + 𝑦) = (𝑡 + ))
102101fveq2d 5996 . . . . . . . . . . . . . . . 16 (𝑦 = → (norm‘(𝑡 + 𝑦)) = (norm‘(𝑡 + )))
103102oveq2d 6447 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑣 · (norm‘(𝑡 + 𝑦))) = (𝑣 · (norm‘(𝑡 + ))))
104100, 103breq12d 4494 . . . . . . . . . . . . . 14 (𝑦 = → (((norm𝑡) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑡 + 𝑦))) ↔ ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + )))))
10598, 104cbvral2v 3059 . . . . . . . . . . . . 13 (∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))))
106 oveq1 6438 . . . . . . . . . . . . . . 15 (𝑣 = (𝑓 + 𝑔) → (𝑣 · (norm‘(𝑡 + ))) = ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))
107106breq2d 4493 . . . . . . . . . . . . . 14 (𝑣 = (𝑓 + 𝑔) → (((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
1081072ralbidv 2876 . . . . . . . . . . . . 13 (𝑣 = (𝑓 + 𝑔) → (∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
109105, 108syl5bb 270 . . . . . . . . . . . 12 (𝑣 = (𝑓 + 𝑔) → (∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
11092, 109anbi12d 742 . . . . . . . . . . 11 (𝑣 = (𝑓 + 𝑔) → ((0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) ↔ (0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))))
111110rspcev 3186 . . . . . . . . . 10 (((𝑓 + 𝑔) ∈ ℝ ∧ (0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))))
112111ex 448 . . . . . . . . 9 ((𝑓 + 𝑔) ∈ ℝ → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11391, 112syl 17 . . . . . . . 8 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
114113adantl 480 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11533, 90, 114syl2and 498 . . . . . 6 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (((0 < 𝑓 ∧ 0 < 𝑔) ∧ (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11630, 115syl5bi 230 . . . . 5 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
117116rexlimdvva 2924 . . . 4 ((𝐴𝐵) = 0 → (∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11829, 117syl5bi 230 . . 3 ((𝐴𝐵) = 0 → ((𝜑𝜓) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
1191183impib 1253 . 2 (((𝐴𝐵) = 0𝜑𝜓) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))))
12012, 119impbii 197 1 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) ↔ ((𝐴𝐵) = 0𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1938  wral 2800  wrex 2801  cin 3443   class class class wbr 4481  cmpt 4541  cfv 5694  crio 6392  (class class class)co 6431  cc 9693  cr 9694  0cc0 9695   + caddc 9698   · cmul 9700   < clt 9833  cle 9834  chil 26942   + cva 26943  normcno 26946   S csh 26951   + cph 26954  0c0h 26958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6728  ax-cnex 9751  ax-resscn 9752  ax-1cn 9753  ax-icn 9754  ax-addcl 9755  ax-addrcl 9756  ax-mulcl 9757  ax-mulrcl 9758  ax-mulcom 9759  ax-addass 9760  ax-mulass 9761  ax-distr 9762  ax-i2m1 9763  ax-1ne0 9764  ax-1rid 9765  ax-rnegex 9766  ax-rrecex 9767  ax-cnre 9768  ax-pre-lttri 9769  ax-pre-lttrn 9770  ax-pre-ltadd 9771  ax-pre-mulgt0 9772  ax-pre-sup 9773  ax-hilex 27022  ax-hfvadd 27023  ax-hvcom 27024  ax-hvass 27025  ax-hv0cl 27026  ax-hvaddid 27027  ax-hfvmul 27028  ax-hvmulid 27029  ax-hvmulass 27030  ax-hvdistr1 27031  ax-hvdistr2 27032  ax-hvmul0 27033  ax-hfi 27102  ax-his1 27105  ax-his3 27107  ax-his4 27108
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5658  df-fun 5696  df-fn 5697  df-f 5698  df-f1 5699  df-fo 5700  df-f1o 5701  df-fv 5702  df-riota 6393  df-ov 6434  df-oprab 6435  df-mpt2 6436  df-om 6839  df-2nd 6940  df-wrecs 7174  df-recs 7235  df-rdg 7273  df-er 7509  df-en 7722  df-dom 7723  df-sdom 7724  df-sup 8111  df-pnf 9835  df-mnf 9836  df-xr 9837  df-ltxr 9838  df-le 9839  df-sub 10022  df-neg 10023  df-div 10437  df-nn 10779  df-2 10837  df-3 10838  df-n0 11051  df-z 11122  df-uz 11431  df-rp 11578  df-seq 12535  df-exp 12594  df-cj 13549  df-re 13550  df-im 13551  df-sqrt 13685  df-abs 13686  df-grpo 26463  df-ablo 26518  df-hnorm 26991  df-hvsub 26994  df-sh 27230  df-ch0 27276  df-shs 27333
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator