Metamath Proof Explorer

Theorem nmfnleub

Description: An upper bound for the norm of a functional. (Contributed by NM, 24-May-2006) (Revised by Mario Carneiro, 7-Sep-2014) (New usage is discouraged.)

Ref Expression
Assertion nmfnleub ⊢T:ℋ⟶ℂ∧A∈ℝ*→normfn⁡T≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A

Proof

Step Hyp Ref Expression
1 nmfnval ⊢T:ℋ⟶ℂ→normfn⁡T=supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<
2 1 adantr ⊢T:ℋ⟶ℂ∧A∈ℝ*→normfn⁡T=supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<
3 2 breq1d ⊢T:ℋ⟶ℂ∧A∈ℝ*→normfn⁡T≤A↔supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<≤A
4 nmfnsetre ⊢T:ℋ⟶ℂ→y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡x⊆ℝ
5 ressxr ⊢ℝ⊆ℝ*
6 4 5 sstrdi ⊢T:ℋ⟶ℂ→y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡x⊆ℝ*
7 supxrleub ⊢y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡x⊆ℝ*∧A∈ℝ*→supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<≤A↔∀z∈y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xz≤A
8 6 7 sylan ⊢T:ℋ⟶ℂ∧A∈ℝ*→supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<≤A↔∀z∈y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xz≤A
9 ancom ⊢normℎ⁡x≤1∧y=T⁡x↔y=T⁡x∧normℎ⁡x≤1
10 eqeq1 ⊢y=z→y=T⁡x↔z=T⁡x
11 10 anbi1d ⊢y=z→y=T⁡x∧normℎ⁡x≤1↔z=T⁡x∧normℎ⁡x≤1
12 9 11 bitrid ⊢y=z→normℎ⁡x≤1∧y=T⁡x↔z=T⁡x∧normℎ⁡x≤1
13 12 rexbidv ⊢y=z→∃x∈ℋnormℎ⁡x≤1∧y=T⁡x↔∃x∈ℋz=T⁡x∧normℎ⁡x≤1
14 13 ralab ⊢∀z∈y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xz≤A↔∀z∃x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A
15 ralcom4 ⊢∀x∈ℋ∀zz=T⁡x∧normℎ⁡x≤1→z≤A↔∀z∀x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A
16 impexp ⊢z=T⁡x∧normℎ⁡x≤1→z≤A↔z=T⁡x→normℎ⁡x≤1→z≤A
17 16 albii ⊢∀zz=T⁡x∧normℎ⁡x≤1→z≤A↔∀zz=T⁡x→normℎ⁡x≤1→z≤A
18 fvex ⊢T⁡x∈V
19 breq1 ⊢z=T⁡x→z≤A↔T⁡x≤A
20 19 imbi2d ⊢z=T⁡x→normℎ⁡x≤1→z≤A↔normℎ⁡x≤1→T⁡x≤A
21 18 20 ceqsalv ⊢∀zz=T⁡x→normℎ⁡x≤1→z≤A↔normℎ⁡x≤1→T⁡x≤A
22 17 21 bitri ⊢∀zz=T⁡x∧normℎ⁡x≤1→z≤A↔normℎ⁡x≤1→T⁡x≤A
23 22 ralbii ⊢∀x∈ℋ∀zz=T⁡x∧normℎ⁡x≤1→z≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A
24 r19.23v ⊢∀x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A↔∃x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A
25 24 albii ⊢∀z∀x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A↔∀z∃x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A
26 15 23 25 3bitr3i ⊢∀x∈ℋnormℎ⁡x≤1→T⁡x≤A↔∀z∃x∈ℋz=T⁡x∧normℎ⁡x≤1→z≤A
27 14 26 bitr4i ⊢∀z∈y|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xz≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A
28 8 27 bitrdi ⊢T:ℋ⟶ℂ∧A∈ℝ*→supy|∃x∈ℋnormℎ⁡x≤1∧y=T⁡xℝ*<≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A
29 3 28 bitrd ⊢T:ℋ⟶ℂ∧A∈ℝ*→normfn⁡T≤A↔∀x∈ℋnormℎ⁡x≤1→T⁡x≤A