Step |
Hyp |
Ref |
Expression |
1 |
|
nmopval |
⊢ ( 𝑇 : ℋ ⟶ ℋ → ( normop ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( normop ‘ 𝑇 ) = sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ) |
3 |
2
|
breq1d |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( ( normop ‘ 𝑇 ) ≤ 𝐴 ↔ sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ) ) |
4 |
|
nmopsetretALT |
⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ ) |
5 |
|
ressxr |
⊢ ℝ ⊆ ℝ* |
6 |
4 5
|
sstrdi |
⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ* ) |
7 |
|
supxrleub |
⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) ) |
8 |
6 7
|
sylan |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ) ) |
9 |
|
ancom |
⊢ ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) |
10 |
|
eqeq1 |
⊢ ( 𝑦 = 𝑧 → ( 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ↔ 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ) |
11 |
10
|
anbi1d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ↔ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) ) |
12 |
9 11
|
syl5bb |
⊢ ( 𝑦 = 𝑧 → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) ) |
13 |
12
|
rexbidv |
⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) ↔ ∃ 𝑥 ∈ ℋ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) ) ) |
14 |
13
|
ralab |
⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ) |
15 |
|
ralcom4 |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ∀ 𝑥 ∈ ℋ ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ) |
16 |
|
impexp |
⊢ ( ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) ) |
17 |
16
|
albii |
⊢ ( ∀ 𝑧 ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) ) |
18 |
|
fvex |
⊢ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∈ V |
19 |
|
breq1 |
⊢ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) → ( 𝑧 ≤ 𝐴 ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) |
20 |
19
|
imbi2d |
⊢ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( ( normℎ ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ↔ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ) |
21 |
18 20
|
ceqsalv |
⊢ ( ∀ 𝑧 ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) → ( ( normℎ ‘ 𝑥 ) ≤ 1 → 𝑧 ≤ 𝐴 ) ) ↔ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) |
22 |
17 21
|
bitri |
⊢ ( ∀ 𝑧 ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) |
23 |
22
|
ralbii |
⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) |
24 |
|
r19.23v |
⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ) |
25 |
24
|
albii |
⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ ℋ ( ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ) |
26 |
15 23 25
|
3bitr3i |
⊢ ( ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ↔ ∀ 𝑧 ( ∃ 𝑥 ∈ ℋ ( 𝑧 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ∧ ( normℎ ‘ 𝑥 ) ≤ 1 ) → 𝑧 ≤ 𝐴 ) ) |
27 |
14 26
|
bitr4i |
⊢ ( ∀ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } 𝑧 ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) |
28 |
8 27
|
syl6bb |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( sup ( { 𝑦 ∣ ∃ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 ∧ 𝑦 = ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ) } , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ) |
29 |
3 28
|
bitrd |
⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝐴 ∈ ℝ* ) → ( ( normop ‘ 𝑇 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ℋ ( ( normℎ ‘ 𝑥 ) ≤ 1 → ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ 𝐴 ) ) ) |