Metamath Proof Explorer

Theorem nmounbi

Description: Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢ X = BaseSet ⁡ U
nmoubi.y ⊢ Y = BaseSet ⁡ W
nmoubi.l ⊢ L = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmounbi ⊢ T : X ⟶ Y → N ⁡ T = +∞ ↔ ∀ r ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ X = BaseSet ⁡ U
2 nmoubi.y ⊢ Y = BaseSet ⁡ W
3 nmoubi.l ⊢ L = norm CV ⁡ U
4 nmoubi.m ⊢ M = norm CV ⁡ W
5 nmoubi.3 ⊢ N = U normOp OLD W
6 nmoubi.u ⊢ U ∈ NrmCVec
7 nmoubi.w ⊢ W ∈ NrmCVec
8 1 2 3 4 5 6 7 nmobndi ⊢ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ ∃ r ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r
9 1 2 5 nmorepnf ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T ≠ +∞
10 6 7 9 mp3an12 ⊢ T : X ⟶ Y → N ⁡ T ∈ ℝ ↔ N ⁡ T ≠ +∞
11 ffvelcdm ⊢ T : X ⟶ Y ∧ y ∈ X → T ⁡ y ∈ Y
12 2 4 nvcl ⊢ W ∈ NrmCVec ∧ T ⁡ y ∈ Y → M ⁡ T ⁡ y ∈ ℝ
13 7 11 12 sylancr ⊢ T : X ⟶ Y ∧ y ∈ X → M ⁡ T ⁡ y ∈ ℝ
14 lenlt ⊢ M ⁡ T ⁡ y ∈ ℝ ∧ r ∈ ℝ → M ⁡ T ⁡ y ≤ r ↔ ¬ r < M ⁡ T ⁡ y
15 13 14 sylan ⊢ T : X ⟶ Y ∧ y ∈ X ∧ r ∈ ℝ → M ⁡ T ⁡ y ≤ r ↔ ¬ r < M ⁡ T ⁡ y
16 15 an32s ⊢ T : X ⟶ Y ∧ r ∈ ℝ ∧ y ∈ X → M ⁡ T ⁡ y ≤ r ↔ ¬ r < M ⁡ T ⁡ y
17 16 imbi2d ⊢ T : X ⟶ Y ∧ r ∈ ℝ ∧ y ∈ X → L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ L ⁡ y ≤ 1 → ¬ r < M ⁡ T ⁡ y
18 imnan ⊢ L ⁡ y ≤ 1 → ¬ r < M ⁡ T ⁡ y ↔ ¬ L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
19 17 18 bitrdi ⊢ T : X ⟶ Y ∧ r ∈ ℝ ∧ y ∈ X → L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ ¬ L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
20 19 ralbidva ⊢ T : X ⟶ Y ∧ r ∈ ℝ → ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ ∀ y ∈ X ¬ L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
21 ralnex ⊢ ∀ y ∈ X ¬ L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y ↔ ¬ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
22 20 21 bitrdi ⊢ T : X ⟶ Y ∧ r ∈ ℝ → ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ ¬ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
23 22 rexbidva ⊢ T : X ⟶ Y → ∃ r ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ ∃ r ∈ ℝ ¬ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
24 rexnal ⊢ ∃ r ∈ ℝ ¬ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y ↔ ¬ ∀ r ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
25 23 24 bitrdi ⊢ T : X ⟶ Y → ∃ r ∈ ℝ ∀ y ∈ X L ⁡ y ≤ 1 → M ⁡ T ⁡ y ≤ r ↔ ¬ ∀ r ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
26 8 10 25 3bitr3d ⊢ T : X ⟶ Y → N ⁡ T ≠ +∞ ↔ ¬ ∀ r ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y
27 26 necon4abid ⊢ T : X ⟶ Y → N ⁡ T = +∞ ↔ ∀ r ∈ ℝ ∃ y ∈ X L ⁡ y ≤ 1 ∧ r < M ⁡ T ⁡ y