Step | Hyp | Ref
| Expression |
1 | | unoplin 28163 |
. . . . 5
⊢ (𝑇 ∈ UniOp → 𝑇 ∈ LinOp) |
2 | | lnopf 28102 |
. . . . 5
⊢ (𝑇 ∈ LinOp → 𝑇: ℋ⟶
ℋ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝑇 ∈ UniOp → 𝑇: ℋ⟶
ℋ) |
4 | | nmopval 28099 |
. . . 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 28107 |
. . . . . . 7
⊢ (𝑇: ℋ⟶ ℋ →
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ) |
8 | | ressxr 9962 |
. . . . . . 7
⊢ ℝ
⊆ ℝ* |
9 | 7, 8 | syl6ss 3580 |
. . . . . 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 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
13 | 12 | rexri 9976 |
. . . 4
⊢ 1 ∈
ℝ* |
14 | 11, 13 | jctir 559 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1
∈ ℝ*)) |
15 | | vex 3176 |
. . . . . . 7
⊢ 𝑧 ∈ V |
16 | | eqeq1 2614 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘(𝑇‘𝑦)))) |
17 | 16 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))))) |
18 | 17 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))))) |
19 | 15, 18 | elab 3319 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))) |
20 | | unopnorm 28160 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
21 | 20 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) → (𝑧 =
(normℎ‘(𝑇‘𝑦)) ↔ 𝑧 = (normℎ‘𝑦))) |
22 | 21 | anbi2d 736 |
. . . . . . . . 9
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦)))) |
23 | | breq1 4586 |
. . . . . . . . . 10
⊢ (𝑧 =
(normℎ‘𝑦) → (𝑧 ≤ 1 ↔
(normℎ‘𝑦) ≤ 1)) |
24 | 23 | biimparc 503 |
. . . . . . . . 9
⊢
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘𝑦)) → 𝑧 ≤ 1) |
25 | 22, 24 | syl6bi 242 |
. . . . . . . 8
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1)) |
26 | 25 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝑇 ∈ UniOp →
(∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦))) → 𝑧 ≤ 1)) |
27 | 26 | imp 444 |
. . . . . 6
⊢ ((𝑇 ∈ UniOp ∧ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑧 = (normℎ‘(𝑇‘𝑦)))) → 𝑧 ≤ 1) |
28 | 19, 27 | sylan2b 491 |
. . . . 5
⊢ ((𝑇 ∈ UniOp ∧ 𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) → 𝑧 ≤ 1) |
29 | 28 | ralrimiva 2949 |
. . . 4
⊢ (𝑇 ∈ UniOp →
∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1) |
30 | 29 | adantl 481 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1) |
31 | | hne0 27790 |
. . . . . . . . . . 11
⊢ ( ℋ
≠ 0ℋ ↔ ∃𝑦 ∈ ℋ 𝑦 ≠ 0ℎ) |
32 | | norm1hex 27492 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℋ 𝑦 ≠
0ℎ ↔ ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
33 | 31, 32 | sylbb 208 |
. . . . . . . . . 10
⊢ ( ℋ
≠ 0ℋ → ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1) |
35 | | 1le1 10534 |
. . . . . . . . . . . . . 14
⊢ 1 ≤
1 |
36 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ↔ 1 ≤ 1)) |
37 | 35, 36 | mpbiri 247 |
. . . . . . . . . . . . 13
⊢
((normℎ‘𝑦) = 1 →
(normℎ‘𝑦) ≤ 1) |
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
(normℎ‘𝑦) ≤ 1)) |
39 | 20 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
(normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦)) |
40 | | eqeq2 2621 |
. . . . . . . . . . . . . . . 16
⊢
((normℎ‘𝑦) = 1 →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(𝑇‘𝑦)) = 1)) |
41 | 40 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
((normℎ‘(𝑇‘𝑦)) = (normℎ‘𝑦) ↔
(normℎ‘(𝑇‘𝑦)) = 1)) |
42 | 39, 41 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) →
(normℎ‘(𝑇‘𝑦)) = 1) |
43 | 42 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) ∧
(normℎ‘𝑦) = 1) → 1 =
(normℎ‘(𝑇‘𝑦))) |
44 | 43 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 → 1 =
(normℎ‘(𝑇‘𝑦)))) |
45 | 38, 44 | jcad 554 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ UniOp ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
46 | 45 | adantll 746 |
. . . . . . . . . 10
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑦 ∈ ℋ) →
((normℎ‘𝑦) = 1 →
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
47 | 46 | reximdva 3000 |
. . . . . . . . 9
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → (∃𝑦 ∈ ℋ
(normℎ‘𝑦) = 1 → ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
48 | 34, 47 | mpd 15 |
. . . . . . . 8
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦)))) |
49 | | 1ex 9914 |
. . . . . . . . 9
⊢ 1 ∈
V |
50 | | eqeq1 2614 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (𝑥 = (normℎ‘(𝑇‘𝑦)) ↔ 1 =
(normℎ‘(𝑇‘𝑦)))) |
51 | 50 | anbi2d 736 |
. . . . . . . . . 10
⊢ (𝑥 = 1 →
(((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
52 | 51 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦))) ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦))))) |
53 | 49, 52 | elab 3319 |
. . . . . . . 8
⊢ (1 ∈
{𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ↔ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 1 =
(normℎ‘(𝑇‘𝑦)))) |
54 | 48, 53 | sylibr 223 |
. . . . . . 7
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) |
55 | 54 | adantr 480 |
. . . . . 6
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → 1 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}) |
56 | | breq2 4587 |
. . . . . . 7
⊢ (𝑤 = 1 → (𝑧 < 𝑤 ↔ 𝑧 < 1)) |
57 | 56 | rspcev 3282 |
. . . . . 6
⊢ ((1
∈ {𝑥 ∣
∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤) |
58 | 55, 57 | sylan 487 |
. . . . 5
⊢ ((((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) ∧ 𝑧 < 1) → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤) |
59 | 58 | ex 449 |
. . . 4
⊢ (((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) ∧ 𝑧 ∈ ℝ) → (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)) |
60 | 59 | ralrimiva 2949 |
. . 3
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤)) |
61 | | supxr2 12016 |
. . 3
⊢ ((({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))} ⊆ ℝ* ∧ 1
∈ ℝ*) ∧ (∀𝑧 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 ≤ 1 ∧ ∀𝑧 ∈ ℝ (𝑧 < 1 → ∃𝑤 ∈ {𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}𝑧 < 𝑤))) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) =
1) |
62 | 14, 30, 60, 61 | syl12anc 1316 |
. 2
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) → sup({𝑥 ∣ ∃𝑦 ∈ ℋ
((normℎ‘𝑦) ≤ 1 ∧ 𝑥 = (normℎ‘(𝑇‘𝑦)))}, ℝ*, < ) =
1) |
63 | 6, 62 | eqtrd 2644 |
1
⊢ ((
ℋ ≠ 0ℋ ∧ 𝑇 ∈ UniOp) →
(normop‘𝑇)
= 1) |