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

Theorem cdj3i 30220
 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 30213 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → (𝐴𝐵) = 0)
4 cdj3.3 . . . . 5 𝑆 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑧𝐴𝑤𝐵 𝑥 = (𝑧 + 𝑤)))
51, 2, 4cdj3lem2b 30216 . . . 4 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))))
6 cdj3.5 . . . 4 (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))))
75, 6sylibr 237 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → 𝜑)
8 cdj3.4 . . . . 5 𝑇 = (𝑥 ∈ (𝐴 + 𝐵) ↦ (𝑤𝐵𝑧𝐴 𝑥 = (𝑧 + 𝑤)))
91, 2, 8cdj3lem3b 30219 . . . 4 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))))
10 cdj3.6 . . . 4 (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))))
119, 10sylibr 237 . . 3 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → 𝜓)
123, 7, 113jca 1125 . 2 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) → ((𝐴𝐵) = 0𝜑𝜓))
13 breq2 5056 . . . . . . . . 9 (𝑣 = 𝑓 → (0 < 𝑣 ↔ 0 < 𝑓))
14 oveq1 7152 . . . . . . . . . . 11 (𝑣 = 𝑓 → (𝑣 · (norm𝑢)) = (𝑓 · (norm𝑢)))
1514breq2d 5064 . . . . . . . . . 10 (𝑣 = 𝑓 → ((norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ (norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
1615ralbidv 3192 . . . . . . . . 9 (𝑣 = 𝑓 → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
1713, 16anbi12d 633 . . . . . . . 8 (𝑣 = 𝑓 → ((0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)))))
1817cbvrexvw 3436 . . . . . . 7 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ ∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
196, 18bitri 278 . . . . . 6 (𝜑 ↔ ∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))))
20 breq2 5056 . . . . . . . . 9 (𝑣 = 𝑔 → (0 < 𝑣 ↔ 0 < 𝑔))
21 oveq1 7152 . . . . . . . . . . 11 (𝑣 = 𝑔 → (𝑣 · (norm𝑢)) = (𝑔 · (norm𝑢)))
2221breq2d 5064 . . . . . . . . . 10 (𝑣 = 𝑔 → ((norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ (norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2322ralbidv 3192 . . . . . . . . 9 (𝑣 = 𝑔 → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢)) ↔ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2420, 23anbi12d 633 . . . . . . . 8 (𝑣 = 𝑔 → ((0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
2524cbvrexvw 3436 . . . . . . 7 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑣 · (norm𝑢))) ↔ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2610, 25bitri 278 . . . . . 6 (𝜓 ↔ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))))
2719, 26anbi12i 629 . . . . 5 ((𝜑𝜓) ↔ (∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
28 reeanv 3359 . . . . 5 (∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) ↔ (∃𝑓 ∈ ℝ (0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ ∃𝑔 ∈ ℝ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
2927, 28bitr4i 281 . . . 4 ((𝜑𝜓) ↔ ∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
30 an4 655 . . . . . 6 (((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) ↔ ((0 < 𝑓 ∧ 0 < 𝑔) ∧ (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))))
31 addgt0 11118 . . . . . . . . 9 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (0 < 𝑓 ∧ 0 < 𝑔)) → 0 < (𝑓 + 𝑔))
3231ex 416 . . . . . . . 8 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → ((0 < 𝑓 ∧ 0 < 𝑔) → 0 < (𝑓 + 𝑔)))
3332adantl 485 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((0 < 𝑓 ∧ 0 < 𝑔) → 0 < (𝑓 + 𝑔)))
341, 2shsvai 29143 . . . . . . . . . . 11 ((𝑡𝐴𝐵) → (𝑡 + ) ∈ (𝐴 + 𝐵))
35 2fveq3 6663 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (norm‘(𝑆𝑢)) = (norm‘(𝑆‘(𝑡 + ))))
36 fveq2 6658 . . . . . . . . . . . . . . 15 (𝑢 = (𝑡 + ) → (norm𝑢) = (norm‘(𝑡 + )))
3736oveq2d 7161 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (𝑓 · (norm𝑢)) = (𝑓 · (norm‘(𝑡 + ))))
3835, 37breq12d 5065 . . . . . . . . . . . . 13 (𝑢 = (𝑡 + ) → ((norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ↔ (norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + )))))
3938rspcv 3604 . . . . . . . . . . . 12 ((𝑡 + ) ∈ (𝐴 + 𝐵) → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) → (norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + )))))
40 2fveq3 6663 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (norm‘(𝑇𝑢)) = (norm‘(𝑇‘(𝑡 + ))))
4136oveq2d 7161 . . . . . . . . . . . . . 14 (𝑢 = (𝑡 + ) → (𝑔 · (norm𝑢)) = (𝑔 · (norm‘(𝑡 + ))))
4240, 41breq12d 5065 . . . . . . . . . . . . 13 (𝑢 = (𝑡 + ) → ((norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)) ↔ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))))
4342rspcv 3604 . . . . . . . . . . . 12 ((𝑡 + ) ∈ (𝐴 + 𝐵) → (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)) → (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))))
4439, 43anim12d 611 . . . . . . . . . . 11 ((𝑡 + ) ∈ (𝐴 + 𝐵) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
4534, 44syl 17 . . . . . . . . . 10 ((𝑡𝐴𝐵) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
4645adantl 485 . . . . . . . . 9 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))))))
471sheli 28993 . . . . . . . . . . . . . . 15 (𝑡𝐴𝑡 ∈ ℋ)
48 normcl 28904 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℋ → (norm𝑡) ∈ ℝ)
4947, 48syl 17 . . . . . . . . . . . . . 14 (𝑡𝐴 → (norm𝑡) ∈ ℝ)
502sheli 28993 . . . . . . . . . . . . . . 15 (𝐵 ∈ ℋ)
51 normcl 28904 . . . . . . . . . . . . . . 15 ( ∈ ℋ → (norm) ∈ ℝ)
5250, 51syl 17 . . . . . . . . . . . . . 14 (𝐵 → (norm) ∈ ℝ)
5349, 52anim12i 615 . . . . . . . . . . . . 13 ((𝑡𝐴𝐵) → ((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ))
5453adantl 485 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → ((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ))
55 hvaddcl 28791 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℋ ∧ ∈ ℋ) → (𝑡 + ) ∈ ℋ)
5647, 50, 55syl2an 598 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵) → (𝑡 + ) ∈ ℋ)
57 normcl 28904 . . . . . . . . . . . . . . 15 ((𝑡 + ) ∈ ℋ → (norm‘(𝑡 + )) ∈ ℝ)
5856, 57syl 17 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵) → (norm‘(𝑡 + )) ∈ ℝ)
59 remulcl 10614 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℝ ∧ (norm‘(𝑡 + )) ∈ ℝ) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
6058, 59sylan2 595 . . . . . . . . . . . . 13 ((𝑓 ∈ ℝ ∧ (𝑡𝐴𝐵)) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
6160adantlr 714 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (𝑓 · (norm‘(𝑡 + ))) ∈ ℝ)
62 remulcl 10614 . . . . . . . . . . . . . 14 ((𝑔 ∈ ℝ ∧ (norm‘(𝑡 + )) ∈ ℝ) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
6358, 62sylan2 595 . . . . . . . . . . . . 13 ((𝑔 ∈ ℝ ∧ (𝑡𝐴𝐵)) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
6463adantll 713 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)
65 le2add 11114 . . . . . . . . . . . 12 ((((norm𝑡) ∈ ℝ ∧ (norm) ∈ ℝ) ∧ ((𝑓 · (norm‘(𝑡 + ))) ∈ ℝ ∧ (𝑔 · (norm‘(𝑡 + ))) ∈ ℝ)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
6654, 61, 64, 65syl12anc 835 . . . . . . . . . . 11 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
6766adantll 713 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
681, 2, 4cdj3lem2 30214 . . . . . . . . . . . . . . . 16 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (𝑆‘(𝑡 + )) = 𝑡)
6968fveq2d 6662 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (norm‘(𝑆‘(𝑡 + ))) = (norm𝑡))
7069breq1d 5062 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → ((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ↔ (norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + )))))
711, 2, 8cdj3lem3 30217 . . . . . . . . . . . . . . . 16 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (𝑇‘(𝑡 + )) = )
7271fveq2d 6662 . . . . . . . . . . . . . . 15 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (norm‘(𝑇‘(𝑡 + ))) = (norm))
7372breq1d 5062 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → ((norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + ))) ↔ (norm) ≤ (𝑔 · (norm‘(𝑡 + )))))
7470, 73anbi12d 633 . . . . . . . . . . . . 13 ((𝑡𝐴𝐵 ∧ (𝐴𝐵) = 0) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
75743expa 1115 . . . . . . . . . . . 12 (((𝑡𝐴𝐵) ∧ (𝐴𝐵) = 0) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
7675ancoms 462 . . . . . . . . . . 11 (((𝐴𝐵) = 0 ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
7776adantlr 714 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) ↔ ((norm𝑡) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm) ≤ (𝑔 · (norm‘(𝑡 + ))))))
78 recn 10619 . . . . . . . . . . . . . 14 (𝑓 ∈ ℝ → 𝑓 ∈ ℂ)
79 recn 10619 . . . . . . . . . . . . . 14 (𝑔 ∈ ℝ → 𝑔 ∈ ℂ)
8058recnd 10661 . . . . . . . . . . . . . 14 ((𝑡𝐴𝐵) → (norm‘(𝑡 + )) ∈ ℂ)
81 adddir 10624 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℂ ∧ 𝑔 ∈ ℂ ∧ (norm‘(𝑡 + )) ∈ ℂ) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
8278, 79, 80, 81syl3an 1157 . . . . . . . . . . . . 13 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ ∧ (𝑡𝐴𝐵)) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
83823expa 1115 . . . . . . . . . . . 12 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) = ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + )))))
8483breq2d 5064 . . . . . . . . . . 11 (((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
8584adantll 713 . . . . . . . . . 10 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 · (norm‘(𝑡 + ))) + (𝑔 · (norm‘(𝑡 + ))))))
8667, 77, 853imtr4d 297 . . . . . . . . 9 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → (((norm‘(𝑆‘(𝑡 + ))) ≤ (𝑓 · (norm‘(𝑡 + ))) ∧ (norm‘(𝑇‘(𝑡 + ))) ≤ (𝑔 · (norm‘(𝑡 + )))) → ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
8746, 86syld 47 . . . . . . . 8 ((((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) ∧ (𝑡𝐴𝐵)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
8887ralrimdvva 3189 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢))) → ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
89 readdcl 10612 . . . . . . . . 9 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → (𝑓 + 𝑔) ∈ ℝ)
90 breq2 5056 . . . . . . . . . . . 12 (𝑣 = (𝑓 + 𝑔) → (0 < 𝑣 ↔ 0 < (𝑓 + 𝑔)))
91 fveq2 6658 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (norm𝑥) = (norm𝑡))
9291oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → ((norm𝑥) + (norm𝑦)) = ((norm𝑡) + (norm𝑦)))
93 fvoveq1 7168 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑡 → (norm‘(𝑥 + 𝑦)) = (norm‘(𝑡 + 𝑦)))
9493oveq2d 7161 . . . . . . . . . . . . . . 15 (𝑥 = 𝑡 → (𝑣 · (norm‘(𝑥 + 𝑦))) = (𝑣 · (norm‘(𝑡 + 𝑦))))
9592, 94breq12d 5065 . . . . . . . . . . . . . 14 (𝑥 = 𝑡 → (((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ((norm𝑡) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑡 + 𝑦)))))
96 fveq2 6658 . . . . . . . . . . . . . . . 16 (𝑦 = → (norm𝑦) = (norm))
9796oveq2d 7161 . . . . . . . . . . . . . . 15 (𝑦 = → ((norm𝑡) + (norm𝑦)) = ((norm𝑡) + (norm)))
98 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑦 = → (𝑡 + 𝑦) = (𝑡 + ))
9998fveq2d 6662 . . . . . . . . . . . . . . . 16 (𝑦 = → (norm‘(𝑡 + 𝑦)) = (norm‘(𝑡 + )))
10099oveq2d 7161 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑣 · (norm‘(𝑡 + 𝑦))) = (𝑣 · (norm‘(𝑡 + ))))
10197, 100breq12d 5065 . . . . . . . . . . . . . 14 (𝑦 = → (((norm𝑡) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑡 + 𝑦))) ↔ ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + )))))
10295, 101cbvral2vw 3447 . . . . . . . . . . . . 13 (∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))))
103 oveq1 7152 . . . . . . . . . . . . . . 15 (𝑣 = (𝑓 + 𝑔) → (𝑣 · (norm‘(𝑡 + ))) = ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))
104103breq2d 5064 . . . . . . . . . . . . . 14 (𝑣 = (𝑓 + 𝑔) → (((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))) ↔ ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
1051042ralbidv 3194 . . . . . . . . . . . . 13 (𝑣 = (𝑓 + 𝑔) → (∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ (𝑣 · (norm‘(𝑡 + ))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
106102, 105syl5bb 286 . . . . . . . . . . . 12 (𝑣 = (𝑓 + 𝑔) → (∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))) ↔ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))))
10790, 106anbi12d 633 . . . . . . . . . . 11 (𝑣 = (𝑓 + 𝑔) → ((0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) ↔ (0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))))
108107rspcev 3609 . . . . . . . . . 10 (((𝑓 + 𝑔) ∈ ℝ ∧ (0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + ))))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))))
109108ex 416 . . . . . . . . 9 ((𝑓 + 𝑔) ∈ ℝ → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11089, 109syl 17 . . . . . . . 8 ((𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ) → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
111110adantl 485 . . . . . . 7 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → ((0 < (𝑓 + 𝑔) ∧ ∀𝑡𝐴𝐵 ((norm𝑡) + (norm)) ≤ ((𝑓 + 𝑔) · (norm‘(𝑡 + )))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11233, 88, 111syl2and 610 . . . . . 6 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (((0 < 𝑓 ∧ 0 < 𝑔) ∧ (∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢)) ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11330, 112syl5bi 245 . . . . 5 (((𝐴𝐵) = 0 ∧ (𝑓 ∈ ℝ ∧ 𝑔 ∈ ℝ)) → (((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
114113rexlimdvva 3287 . . . 4 ((𝐴𝐵) = 0 → (∃𝑓 ∈ ℝ ∃𝑔 ∈ ℝ ((0 < 𝑓 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑆𝑢)) ≤ (𝑓 · (norm𝑢))) ∧ (0 < 𝑔 ∧ ∀𝑢 ∈ (𝐴 + 𝐵)(norm‘(𝑇𝑢)) ≤ (𝑔 · (norm𝑢)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
11529, 114syl5bi 245 . . 3 ((𝐴𝐵) = 0 → ((𝜑𝜓) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦))))))
1161153impib 1113 . 2 (((𝐴𝐵) = 0𝜑𝜓) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))))
11712, 116impbii 212 1 (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥𝐴𝑦𝐵 ((norm𝑥) + (norm𝑦)) ≤ (𝑣 · (norm‘(𝑥 + 𝑦)))) ↔ ((𝐴𝐵) = 0𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134   ∩ cin 3918   class class class wbr 5052   ↦ cmpt 5132  ‘cfv 6343  ℩crio 7102  (class class class)co 7145  ℂcc 10527  ℝcr 10528  0cc0 10529   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   ℋchba 28698   +ℎ cva 28699  normℎcno 28702   Sℋ csh 28707   +ℋ cph 28710  0ℋc0h 28714 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-hilex 28778  ax-hfvadd 28779  ax-hvcom 28780  ax-hvass 28781  ax-hv0cl 28782  ax-hvaddid 28783  ax-hfvmul 28784  ax-hvmulid 28785  ax-hvmulass 28786  ax-hvdistr1 28787  ax-hvdistr2 28788  ax-hvmul0 28789  ax-hfi 28858  ax-his1 28861  ax-his3 28863  ax-his4 28864 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7571  df-2nd 7680  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-er 8279  df-en 8500  df-dom 8501  df-sdom 8502  df-sup 8897  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-n0 11891  df-z 11975  df-uz 12237  df-rp 12383  df-seq 13370  df-exp 13431  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-grpo 28272  df-ablo 28324  df-hnorm 28747  df-hvsub 28750  df-sh 28986  df-ch0 29032  df-shs 29087 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator