Step | Hyp | Ref
| Expression |
1 | | normcl 29487 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
2 | 1 | recnd 11003 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℂ) |
3 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘𝑥) ∈ ℂ) |
4 | | norm-i 29491 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
5 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = (𝑇‘0ℎ)) |
6 | | nmlnop0.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ∈ LinOp |
7 | 6 | lnop0i 30332 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇‘0ℎ) =
0ℎ |
8 | 5, 7 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = 0ℎ) |
9 | 4, 8 | syl6bi 252 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 → (𝑇‘𝑥) = 0ℎ)) |
10 | 9 | necon3d 2964 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ → ((𝑇‘𝑥) ≠ 0ℎ →
(normℎ‘𝑥) ≠ 0)) |
11 | 10 | imp 407 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘𝑥) ≠ 0) |
12 | 3, 11 | recne0d 11745 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (1 /
(normℎ‘𝑥)) ≠ 0) |
13 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘𝑥) ≠ 0ℎ) |
14 | 3, 11 | reccld 11744 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (1 /
(normℎ‘𝑥)) ∈ ℂ) |
15 | 6 | lnopfi 30331 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇: ℋ⟶
ℋ |
16 | 15 | ffvelrni 6960 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘𝑥) ∈ ℋ) |
18 | | hvmul0or 29387 |
. . . . . . . . . . . . . 14
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = 0ℎ ↔ ((1 /
(normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
19 | 14, 17, 18 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = 0ℎ ↔ ((1 /
(normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
20 | 19 | necon3abid 2980 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ ¬ ((1
/ (normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
21 | | neanior 3037 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 0ℎ) ↔ ¬ ((1
/ (normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ)) |
22 | 20, 21 | bitr4di 289 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ ((1 /
(normℎ‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠
0ℎ))) |
23 | 12, 13, 22 | mpbir2and 710 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠
0ℎ) |
24 | | hvmulcl 29375 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
25 | 14, 17, 24 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
26 | | normgt0 29489 |
. . . . . . . . . . 11
⊢ (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
28 | 23, 27 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥)))) |
29 | 28 | ex 413 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ → ((𝑇‘𝑥) ≠ 0ℎ → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
30 | 29 | adantl 482 |
. . . . . . 7
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ≠ 0ℎ → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
31 | | nmopsetretHIL 30226 |
. . . . . . . . . . . . . 14
⊢ (𝑇: ℋ⟶ ℋ →
{𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ) |
32 | 15, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ |
33 | | ressxr 11019 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
34 | 32, 33 | sstri 3930 |
. . . . . . . . . . . 12
⊢ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆
ℝ* |
35 | | simpl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → 𝑥 ∈
ℋ) |
36 | | hvmulcl 29375 |
. . . . . . . . . . . . . . 15
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈
ℋ) |
37 | 14, 35, 36 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈
ℋ) |
38 | 8 | necon3i 2976 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇‘𝑥) ≠ 0ℎ → 𝑥 ≠
0ℎ) |
39 | | norm1 29611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = 1) |
40 | 38, 39 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = 1) |
41 | | 1re 10975 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
42 | 40, 41 | eqeltrdi 2847 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ∈ ℝ) |
43 | | eqle 11077 |
. . . . . . . . . . . . . . 15
⊢
(((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ ℝ ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = 1) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1) |
44 | 42, 40, 43 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1) |
45 | 6 | lnopmuli 30334 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) → (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) |
46 | 14, 35, 45 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) |
47 | 46 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
48 | 47 | fveq2d 6778 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))) |
49 | | fveq2 6774 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(normℎ‘𝑧) = (normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
50 | 49 | breq1d 5084 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
((normℎ‘𝑧) ≤ 1 ↔
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1)) |
51 | | fveq2 6774 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) → (𝑇‘𝑧) = (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
52 | 51 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(normℎ‘(𝑇‘𝑧)) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))) |
53 | 52 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)) ↔ (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))))) |
54 | 50, 53 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))) ↔
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))))) |
55 | 54 | rspcev 3561 |
. . . . . . . . . . . . . 14
⊢ ((((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈ ℋ ∧
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))))) → ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
56 | 37, 44, 48, 55 | syl12anc 834 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
57 | | fvex 6787 |
. . . . . . . . . . . . . 14
⊢
(normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ V |
58 | | eqeq1 2742 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) → (𝑦 = (normℎ‘(𝑇‘𝑧)) ↔ (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
59 | 58 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) →
(((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧))) ↔
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))))) |
60 | 59 | rexbidv 3226 |
. . . . . . . . . . . . . 14
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) → (∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧))) ↔ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))))) |
61 | 57, 60 | elab 3609 |
. . . . . . . . . . . . 13
⊢
((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ↔ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
62 | 56, 61 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}) |
63 | | supxrub 13058 |
. . . . . . . . . . . 12
⊢ (({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ* ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
64 | 34, 62, 63 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
65 | 64 | adantll 711 |
. . . . . . . . . 10
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
66 | | nmopval 30218 |
. . . . . . . . . . . . . 14
⊢ (𝑇: ℋ⟶ ℋ →
(normop‘𝑇)
= sup({𝑦 ∣
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
67 | 15, 66 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(normop‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
) |
68 | 67 | eqeq1i 2743 |
. . . . . . . . . . . 12
⊢
((normop‘𝑇) = 0 ↔ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
69 | 68 | biimpi 215 |
. . . . . . . . . . 11
⊢
((normop‘𝑇) = 0 → sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
70 | 69 | ad2antrr 723 |
. . . . . . . . . 10
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
71 | 65, 70 | breqtrd 5100 |
. . . . . . . . 9
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0) |
72 | | normcl 29487 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ ℝ) |
73 | 25, 72 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ ℝ) |
74 | | 0re 10977 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
75 | | lenlt 11053 |
. . . . . . . . . . 11
⊢
(((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
76 | 73, 74, 75 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
77 | 76 | adantll 711 |
. . . . . . . . 9
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
78 | 71, 77 | mpbid 231 |
. . . . . . . 8
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) → ¬ 0
< (normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥)))) |
79 | 78 | ex 413 |
. . . . . . 7
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ≠ 0ℎ → ¬ 0
< (normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
80 | 30, 79 | pm2.65d 195 |
. . . . . 6
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ¬ (𝑇‘𝑥) ≠ 0ℎ) |
81 | | nne 2947 |
. . . . . 6
⊢ (¬
(𝑇‘𝑥) ≠ 0ℎ ↔ (𝑇‘𝑥) = 0ℎ) |
82 | 80, 81 | sylib 217 |
. . . . 5
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = 0ℎ) |
83 | | ho0val 30112 |
. . . . . 6
⊢ (𝑥 ∈ ℋ → (
0hop ‘𝑥) =
0ℎ) |
84 | 83 | adantl 482 |
. . . . 5
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ( 0hop
‘𝑥) =
0ℎ) |
85 | 82, 84 | eqtr4d 2781 |
. . . 4
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
86 | 85 | ralrimiva 3103 |
. . 3
⊢
((normop‘𝑇) = 0 → ∀𝑥 ∈ ℋ (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
87 | | ffn 6600 |
. . . . 5
⊢ (𝑇: ℋ⟶ ℋ →
𝑇 Fn
ℋ) |
88 | 15, 87 | ax-mp 5 |
. . . 4
⊢ 𝑇 Fn ℋ |
89 | | ho0f 30113 |
. . . . 5
⊢
0hop : ℋ⟶ ℋ |
90 | | ffn 6600 |
. . . . 5
⊢ (
0hop : ℋ⟶ ℋ → 0hop Fn
ℋ) |
91 | 89, 90 | ax-mp 5 |
. . . 4
⊢
0hop Fn ℋ |
92 | | eqfnfv 6909 |
. . . 4
⊢ ((𝑇 Fn ℋ ∧
0hop Fn ℋ) → (𝑇 = 0hop ↔ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = ( 0hop ‘𝑥))) |
93 | 88, 91, 92 | mp2an 689 |
. . 3
⊢ (𝑇 = 0hop ↔
∀𝑥 ∈ ℋ
(𝑇‘𝑥) = ( 0hop ‘𝑥)) |
94 | 86, 93 | sylibr 233 |
. 2
⊢
((normop‘𝑇) = 0 → 𝑇 = 0hop ) |
95 | | fveq2 6774 |
. . 3
⊢ (𝑇 = 0hop →
(normop‘𝑇)
= (normop‘ 0hop )) |
96 | | nmop0 30348 |
. . 3
⊢
(normop‘ 0hop ) = 0 |
97 | 95, 96 | eqtrdi 2794 |
. 2
⊢ (𝑇 = 0hop →
(normop‘𝑇)
= 0) |
98 | 94, 97 | impbii 208 |
1
⊢
((normop‘𝑇) = 0 ↔ 𝑇 = 0hop ) |