| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nmfnval 31895 | . . . 4
⊢ (𝑇: ℋ⟶ℂ →
(normfn‘𝑇)
= sup({𝑦 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, <
)) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → (normfn‘𝑇) = sup({𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, <
)) | 
| 3 | 2 | breq1d 5153 | . 2
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ sup({𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, < ) ≤ 𝐴)) | 
| 4 |  | nmfnsetre 31896 | . . . . 5
⊢ (𝑇: ℋ⟶ℂ →
{𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))} ⊆ ℝ) | 
| 5 |  | ressxr 11305 | . . . . 5
⊢ ℝ
⊆ ℝ* | 
| 6 | 4, 5 | sstrdi 3996 | . . . 4
⊢ (𝑇: ℋ⟶ℂ →
{𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))} ⊆
ℝ*) | 
| 7 |  | supxrleub 13368 | . . . 4
⊢ (({𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))} ⊆ ℝ* ∧ 𝐴 ∈ ℝ*)
→ (sup({𝑦 ∣
∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, < ) ≤ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}𝑧 ≤ 𝐴)) | 
| 8 | 6, 7 | sylan 580 | . . 3
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → (sup({𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, < ) ≤ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}𝑧 ≤ 𝐴)) | 
| 9 |  | ancom 460 | . . . . . . 7
⊢
(((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥))) ↔ (𝑦 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1)) | 
| 10 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑦 = (abs‘(𝑇‘𝑥)) ↔ 𝑧 = (abs‘(𝑇‘𝑥)))) | 
| 11 | 10 | anbi1d 631 | . . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑦 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) ↔ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1))) | 
| 12 | 9, 11 | bitrid 283 | . . . . . 6
⊢ (𝑦 = 𝑧 →
(((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥))) ↔ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1))) | 
| 13 | 12 | rexbidv 3179 | . . . . 5
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥))) ↔ ∃𝑥 ∈ ℋ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1))) | 
| 14 | 13 | ralab 3697 | . . . 4
⊢
(∀𝑧 ∈
{𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}𝑧 ≤ 𝐴 ↔ ∀𝑧(∃𝑥 ∈ ℋ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴)) | 
| 15 |  | ralcom4 3286 | . . . . 5
⊢
(∀𝑥 ∈
ℋ ∀𝑧((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ ∀𝑧∀𝑥 ∈ ℋ ((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴)) | 
| 16 |  | impexp 450 | . . . . . . . 8
⊢ (((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ (𝑧 = (abs‘(𝑇‘𝑥)) →
((normℎ‘𝑥) ≤ 1 → 𝑧 ≤ 𝐴))) | 
| 17 | 16 | albii 1819 | . . . . . . 7
⊢
(∀𝑧((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ ∀𝑧(𝑧 = (abs‘(𝑇‘𝑥)) →
((normℎ‘𝑥) ≤ 1 → 𝑧 ≤ 𝐴))) | 
| 18 |  | fvex 6919 | . . . . . . . 8
⊢
(abs‘(𝑇‘𝑥)) ∈ V | 
| 19 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑧 = (abs‘(𝑇‘𝑥)) → (𝑧 ≤ 𝐴 ↔ (abs‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 20 | 19 | imbi2d 340 | . . . . . . . 8
⊢ (𝑧 = (abs‘(𝑇‘𝑥)) →
(((normℎ‘𝑥) ≤ 1 → 𝑧 ≤ 𝐴) ↔
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 21 | 18, 20 | ceqsalv 3521 | . . . . . . 7
⊢
(∀𝑧(𝑧 = (abs‘(𝑇‘𝑥)) →
((normℎ‘𝑥) ≤ 1 → 𝑧 ≤ 𝐴)) ↔
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 22 | 17, 21 | bitri 275 | . . . . . 6
⊢
(∀𝑧((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 23 | 22 | ralbii 3093 | . . . . 5
⊢
(∀𝑥 ∈
ℋ ∀𝑧((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 24 |  | r19.23v 3183 | . . . . . 6
⊢
(∀𝑥 ∈
ℋ ((𝑧 =
(abs‘(𝑇‘𝑥)) ∧
(normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ (∃𝑥 ∈ ℋ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴)) | 
| 25 | 24 | albii 1819 | . . . . 5
⊢
(∀𝑧∀𝑥 ∈ ℋ ((𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴) ↔ ∀𝑧(∃𝑥 ∈ ℋ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴)) | 
| 26 | 15, 23, 25 | 3bitr3i 301 | . . . 4
⊢
(∀𝑥 ∈
ℋ ((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴) ↔ ∀𝑧(∃𝑥 ∈ ℋ (𝑧 = (abs‘(𝑇‘𝑥)) ∧ (normℎ‘𝑥) ≤ 1) → 𝑧 ≤ 𝐴)) | 
| 27 | 14, 26 | bitr4i 278 | . . 3
⊢
(∀𝑧 ∈
{𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}𝑧 ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 28 | 8, 27 | bitrdi 287 | . 2
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → (sup({𝑦 ∣ ∃𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 ∧ 𝑦 = (abs‘(𝑇‘𝑥)))}, ℝ*, < ) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 29 | 3, 28 | bitrd 279 | 1
⊢ ((𝑇: ℋ⟶ℂ ∧
𝐴 ∈
ℝ*) → ((normfn‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 → (abs‘(𝑇‘𝑥)) ≤ 𝐴))) |