| Step | Hyp | Ref
| Expression |
| 1 | | unoplin 31939 |
. . . . 5
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) |
| 2 | | lnopf 31878 |
. . . . 5
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶
ℋ) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑇 ∈ UniOp → 𝑇: ℋ⟶
ℋ) |
| 4 | | nmopval 31875 |
. . . 4
⊢ (𝑇: ℋ⟶ ℋ →
(normop‘𝑇)
= sup({𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, <
)) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ (𝑇 ∈ UniOp →
(normop‘𝑇)
= sup({𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, <
)) |
| 6 | 5 | adantl 481 |
. 2
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) →
(normop‘𝑇)
= sup({𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, <
)) |
| 7 | | nmopsetretHIL 31883 |
. . . . . . 7
⊢ (𝑇: ℋ⟶ ℋ →
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) |
| 8 | | ressxr 11305 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
| 9 | 7, 8 | sstrdi 3996 |
. . . . . 6
⊢ (𝑇: ℋ⟶ ℋ →
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆
ℝ*) |
| 10 | 3, 9 | syl 17 |
. . . . 5
⊢ (𝑇 ∈ UniOp → {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆
ℝ*) |
| 11 | 10 | adantl 481 |
. . . 4
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆
ℝ*) |
| 12 | | 1xr 11320 |
. . . 4
⊢ 1 ∈
ℝ* |
| 13 | 11, 12 | jctir 520 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1
∈ ℝ*)) |
| 14 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 15 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘(𝑇‘𝑦)))) |
| 16 | 15 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))))) |
| 17 | 16 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))))) |
| 18 | 14, 17 | elab 3679 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))) |
| 19 | | unopnorm 31936 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
| 20 | 19 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (𝑧 =
(normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘𝑦))) |
| 21 | 20 | anbi2d 630 |
. . . . . . . . 9
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦)))) |
| 22 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑧 =
(normℎ‘𝑦) → (𝑧 ≤ 1 ↔
(normℎ‘𝑦) ≤ 1)) |
| 23 | 22 | biimparc 479 |
. . . . . . . . 9
⊢
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦)) → 𝑧 ≤ 1) |
| 24 | 21, 23 | biimtrdi 253 |
. . . . . . . 8
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1)) |
| 25 | 24 | rexlimdva 3155 |
. . . . . . 7
⊢ (𝑇 ∈ UniOp →
(∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1)) |
| 26 | 25 | imp 406 |
. . . . . 6
⊢ ((𝑇 ∈ UniOp ∧ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))) → 𝑧 ≤ 1) |
| 27 | 18, 26 | sylan2b 594 |
. . . . 5
⊢ ((𝑇 ∈ UniOp ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) → 𝑧 ≤ 1) |
| 28 | 27 | ralrimiva 3146 |
. . . 4
⊢ (𝑇 ∈ UniOp →
∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1) |
| 29 | 28 | adantl 481 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1) |
| 30 | | hne0 31566 |
. . . . . . . . . . 11
⊢ ( ℋ
≠ 0ℋ ↔ ∃𝑦 ∈ ℋ 𝑦 ≠ 0ℎ) |
| 31 | | norm1hex 31270 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℋ 𝑦 ≠
0ℎ ↔ ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
| 32 | 30, 31 | sylbb 219 |
. . . . . . . . . 10
⊢ ( ℋ
≠ 0ℋ → ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
| 33 | 32 | adantr 480 |
. . . . . . . . 9
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
| 34 | | 1le1 11891 |
. . . . . . . . . . . . . 14
⊢ 1 ≤
1 |
| 35 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ↔ 1 ≤ 1)) |
| 36 | 34, 35 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢
((normℎ‘𝑦) = 1 →
(normℎ‘𝑦) ≤ 1) |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
(normℎ‘𝑦) ≤ 1)) |
| 38 | 19 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
| 39 | | eqeq2 2749 |
. . . . . . . . . . . . . . . 16
⊢
((normℎ‘𝑦) = 1 →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(𝑇‘𝑦)) = 1)) |
| 40 | 39 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(𝑇‘𝑦)) = 1)) |
| 41 | 38, 40 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
(normℎ‘(𝑇‘𝑦)) = 1) |
| 42 | 41 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) → 1 =
(normℎ‘(𝑇‘𝑦))) |
| 43 | 42 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 → 1 =
(normℎ‘(𝑇‘𝑦)))) |
| 44 | 37, 43 | jcad 512 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
| 45 | 44 | adantll 714 |
. . . . . . . . . 10
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
| 46 | 45 | reximdva 3168 |
. . . . . . . . 9
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1 → ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
| 47 | 33, 46 | mpd 15 |
. . . . . . . 8
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦)))) |
| 48 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 49 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 1 =
(normℎ‘(𝑇‘𝑦)))) |
| 50 | 49 | anbi2d 630 |
. . . . . . . . . 10
⊢ (𝑥 = 1 →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
| 51 | 50 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
| 52 | 48, 51 | elab 3679 |
. . . . . . . 8
⊢ (1 ∈
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦)))) |
| 53 | 47, 52 | sylibr 234 |
. . . . . . 7
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) |
| 54 | 53 | adantr 480 |
. . . . . 6
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) |
| 55 | | breq2 5147 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝑧 < 𝑤 ↔ 𝑧 < 1)) |
| 56 | 55 | rspcev 3622 |
. . . . . 6
⊢ ((1
∈ {𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤) |
| 57 | 54, 56 | sylan 580 |
. . . . 5
⊢ ((((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤) |
| 58 | 57 | ex 412 |
. . . 4
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)) |
| 59 | 58 | ralrimiva 3146 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)) |
| 60 | | supxr2 13356 |
. . 3
⊢ ((({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1
∈ ℝ*) ∧ (∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1 ∧ ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤))) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) =
1) |
| 61 | 13, 29, 59, 60 | syl12anc 837 |
. 2
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) =
1) |
| 62 | 6, 61 | eqtrd 2777 |
1
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) →
(normop‘𝑇)
= 1) |