Step | Hyp | Ref
| Expression |
1 | | normcl 29073 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) |
2 | 1 | recnd 10760 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℂ) |
3 | 2 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘𝑥) ∈ ℂ) |
4 | | norm-i 29077 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 ↔ 𝑥 = 0ℎ)) |
5 | | fveq2 6687 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = (𝑇‘0ℎ)) |
6 | | nmlnop0.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇 ∈ LinOp |
7 | 6 | lnop0i 29918 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇‘0ℎ) =
0ℎ |
8 | 5, 7 | eqtrdi 2790 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0ℎ →
(𝑇‘𝑥) = 0ℎ) |
9 | 4, 8 | syl6bi 256 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) = 0 → (𝑇‘𝑥) = 0ℎ)) |
10 | 9 | necon3d 2956 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ → ((𝑇‘𝑥) ≠ 0ℎ →
(normℎ‘𝑥) ≠ 0)) |
11 | 10 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘𝑥) ≠ 0) |
12 | 3, 11 | recne0d 11501 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (1 /
(normℎ‘𝑥)) ≠ 0) |
13 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘𝑥) ≠ 0ℎ) |
14 | 3, 11 | reccld 11500 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (1 /
(normℎ‘𝑥)) ∈ ℂ) |
15 | 6 | lnopfi 29917 |
. . . . . . . . . . . . . . . 16
⊢ 𝑇: ℋ⟶
ℋ |
16 | 15 | ffvelrni 6873 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ) |
17 | 16 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘𝑥) ∈ ℋ) |
18 | | hvmul0or 28973 |
. . . . . . . . . . . . . 14
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = 0ℎ ↔ ((1 /
(normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
19 | 14, 17, 18 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = 0ℎ ↔ ((1 /
(normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
20 | 19 | necon3abid 2971 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ ¬ ((1
/ (normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ))) |
21 | | neanior 3027 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠ 0ℎ) ↔ ¬ ((1
/ (normℎ‘𝑥)) = 0 ∨ (𝑇‘𝑥) = 0ℎ)) |
22 | 20, 21 | bitr4di 292 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠ 0ℎ ↔ ((1 /
(normℎ‘𝑥)) ≠ 0 ∧ (𝑇‘𝑥) ≠
0ℎ))) |
23 | 12, 13, 22 | mpbir2and 713 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ≠
0ℎ) |
24 | | hvmulcl 28961 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
25 | 14, 17, 24 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
26 | | normgt0 29075 |
. . . . . . . . . . 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 235 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥)))) |
29 | 28 | ex 416 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ → ((𝑇‘𝑥) ≠ 0ℎ → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
30 | 29 | adantl 485 |
. . . . . . 7
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ≠ 0ℎ → 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
31 | | nmopsetretHIL 29812 |
. . . . . . . . . . . . . 14
⊢ (𝑇: ℋ⟶ ℋ →
{𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ) |
32 | 15, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ |
33 | | ressxr 10776 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
34 | 32, 33 | sstri 3896 |
. . . . . . . . . . . 12
⊢ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆
ℝ* |
35 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → 𝑥 ∈
ℋ) |
36 | | hvmulcl 28961 |
. . . . . . . . . . . . . . 15
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈
ℋ) |
37 | 14, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) ∈
ℋ) |
38 | 8 | necon3i 2967 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇‘𝑥) ≠ 0ℎ → 𝑥 ≠
0ℎ) |
39 | | norm1 29197 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = 1) |
40 | 38, 39 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = 1) |
41 | | 1re 10732 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
42 | 40, 41 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ∈ ℝ) |
43 | | eqle 10833 |
. . . . . . . . . . . . . . 15
⊢
(((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) ∈ ℝ ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) = 1) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1) |
44 | 42, 40, 43 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1) |
45 | 6 | lnopmuli 29920 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
(normℎ‘𝑥)) ∈ ℂ ∧ 𝑥 ∈ ℋ) → (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) |
46 | 14, 35, 45 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)) = ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) |
47 | 46 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) → ((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) = (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
48 | 47 | fveq2d 6691 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))) |
49 | | fveq2 6687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(normℎ‘𝑧) = (normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
50 | 49 | breq1d 5050 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
((normℎ‘𝑧) ≤ 1 ↔
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1)) |
51 | | fveq2 6687 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) → (𝑇‘𝑧) = (𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))) |
52 | 51 | fveq2d 6691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(normℎ‘(𝑇‘𝑧)) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))) |
53 | 52 | eqeq2d 2750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)) ↔ (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥))))) |
54 | 50, 53 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((1 /
(normℎ‘𝑥)) ·ℎ 𝑥) →
(((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))) ↔
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ 𝑥)) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘((1 /
(normℎ‘𝑥)) ·ℎ 𝑥)))))) |
55 | 54 | rspcev 3529 |
. . . . . . . . . . . . . 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 836 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
57 | | fvex 6700 |
. . . . . . . . . . . . . 14
⊢
(normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ V |
58 | | eqeq1 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) → (𝑦 = (normℎ‘(𝑇‘𝑧)) ↔ (normℎ‘((1
/ (normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
59 | 58 | anbi2d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) →
(((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧))) ↔
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))))) |
60 | 59 | rexbidv 3208 |
. . . . . . . . . . . . . 14
⊢ (𝑦 =
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) → (∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧))) ↔ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧))))) |
61 | 57, 60 | elab 3578 |
. . . . . . . . . . . . 13
⊢
((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ↔ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) = (normℎ‘(𝑇‘𝑧)))) |
62 | 56, 61 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}) |
63 | | supxrub 12813 |
. . . . . . . . . . . 12
⊢ (({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))} ⊆ ℝ* ∧
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ {𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
64 | 34, 62, 63 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
65 | 64 | adantll 714 |
. . . . . . . . . 10
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
66 | | nmopval 29804 |
. . . . . . . . . . . . . 14
⊢ (𝑇: ℋ⟶ ℋ →
(normop‘𝑇)
= sup({𝑦 ∣
∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
)) |
67 | 15, 66 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(normop‘𝑇) = sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, <
) |
68 | 67 | eqeq1i 2744 |
. . . . . . . . . . . 12
⊢
((normop‘𝑇) = 0 ↔ sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
69 | 68 | biimpi 219 |
. . . . . . . . . . 11
⊢
((normop‘𝑇) = 0 → sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
70 | 69 | ad2antrr 726 |
. . . . . . . . . 10
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
sup({𝑦 ∣ ∃𝑧 ∈ ℋ
((normℎ‘𝑧) ≤ 1 ∧ 𝑦 = (normℎ‘(𝑇‘𝑧)))}, ℝ*, < ) =
0) |
71 | 65, 70 | breqtrd 5066 |
. . . . . . . . 9
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0) |
72 | | normcl 29073 |
. . . . . . . . . . . 12
⊢ (((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥)) ∈ ℋ →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ ℝ) |
73 | 25, 72 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ∈ ℝ) |
74 | | 0re 10734 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
75 | | lenlt 10810 |
. . . . . . . . . . 11
⊢
(((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((normℎ‘((1 /
(normℎ‘𝑥)) ·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
76 | 73, 74, 75 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℋ ∧ (𝑇‘𝑥) ≠ 0ℎ) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
77 | 76 | adantll 714 |
. . . . . . . . 9
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) →
((normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))) ≤ 0 ↔ ¬ 0 <
(normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
78 | 71, 77 | mpbid 235 |
. . . . . . . 8
⊢
((((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) ∧ (𝑇‘𝑥) ≠ 0ℎ) → ¬ 0
< (normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥)))) |
79 | 78 | ex 416 |
. . . . . . 7
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ≠ 0ℎ → ¬ 0
< (normℎ‘((1 / (normℎ‘𝑥))
·ℎ (𝑇‘𝑥))))) |
80 | 30, 79 | pm2.65d 199 |
. . . . . 6
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ¬ (𝑇‘𝑥) ≠ 0ℎ) |
81 | | nne 2939 |
. . . . . 6
⊢ (¬
(𝑇‘𝑥) ≠ 0ℎ ↔ (𝑇‘𝑥) = 0ℎ) |
82 | 80, 81 | sylib 221 |
. . . . 5
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = 0ℎ) |
83 | | ho0val 29698 |
. . . . . 6
⊢ (𝑥 ∈ ℋ → (
0hop ‘𝑥) =
0ℎ) |
84 | 83 | adantl 485 |
. . . . 5
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → ( 0hop
‘𝑥) =
0ℎ) |
85 | 82, 84 | eqtr4d 2777 |
. . . 4
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
86 | 85 | ralrimiva 3097 |
. . 3
⊢
((normop‘𝑇) = 0 → ∀𝑥 ∈ ℋ (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
87 | | ffn 6515 |
. . . . 5
⊢ (𝑇: ℋ⟶ ℋ →
𝑇 Fn
ℋ) |
88 | 15, 87 | ax-mp 5 |
. . . 4
⊢ 𝑇 Fn ℋ |
89 | | ho0f 29699 |
. . . . 5
⊢
0hop : ℋ⟶ ℋ |
90 | | ffn 6515 |
. . . . 5
⊢ (
0hop : ℋ⟶ ℋ → 0hop Fn
ℋ) |
91 | 89, 90 | ax-mp 5 |
. . . 4
⊢
0hop Fn ℋ |
92 | | eqfnfv 6822 |
. . . 4
⊢ ((𝑇 Fn ℋ ∧
0hop Fn ℋ) → (𝑇 = 0hop ↔ ∀𝑥 ∈ ℋ (𝑇‘𝑥) = ( 0hop ‘𝑥))) |
93 | 88, 91, 92 | mp2an 692 |
. . 3
⊢ (𝑇 = 0hop ↔
∀𝑥 ∈ ℋ
(𝑇‘𝑥) = ( 0hop ‘𝑥)) |
94 | 86, 93 | sylibr 237 |
. 2
⊢
((normop‘𝑇) = 0 → 𝑇 = 0hop ) |
95 | | fveq2 6687 |
. . 3
⊢ (𝑇 = 0hop →
(normop‘𝑇)
= (normop‘ 0hop )) |
96 | | nmop0 29934 |
. . 3
⊢
(normop‘ 0hop ) = 0 |
97 | 95, 96 | eqtrdi 2790 |
. 2
⊢ (𝑇 = 0hop →
(normop‘𝑇)
= 0) |
98 | 94, 97 | impbii 212 |
1
⊢
((normop‘𝑇) = 0 ↔ 𝑇 = 0hop ) |