Step | Hyp | Ref
| Expression |
1 | | nmoptri.1 |
. . . . . 6
⊢ 𝑆 ∈
BndLinOp |
2 | | bdopln 29796 |
. . . . . 6
⊢ (𝑆 ∈ BndLinOp → 𝑆 ∈ LinOp) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ 𝑆 ∈ LinOp |
4 | | nmoptri.2 |
. . . . . 6
⊢ 𝑇 ∈
BndLinOp |
5 | | bdopln 29796 |
. . . . . 6
⊢ (𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ 𝑇 ∈ LinOp |
7 | 3, 6 | lnopcoi 29938 |
. . . 4
⊢ (𝑆 ∘ 𝑇) ∈ LinOp |
8 | 7 | lnopfi 29904 |
. . 3
⊢ (𝑆 ∘ 𝑇): ℋ⟶ ℋ |
9 | | nmopre 29805 |
. . . . . 6
⊢ (𝑆 ∈ BndLinOp →
(normop‘𝑆)
∈ ℝ) |
10 | 1, 9 | ax-mp 5 |
. . . . 5
⊢
(normop‘𝑆) ∈ ℝ |
11 | | nmopre 29805 |
. . . . . 6
⊢ (𝑇 ∈ BndLinOp →
(normop‘𝑇)
∈ ℝ) |
12 | 4, 11 | ax-mp 5 |
. . . . 5
⊢
(normop‘𝑇) ∈ ℝ |
13 | 10, 12 | remulcli 10735 |
. . . 4
⊢
((normop‘𝑆) · (normop‘𝑇)) ∈
ℝ |
14 | 13 | rexri 10777 |
. . 3
⊢
((normop‘𝑆) · (normop‘𝑇)) ∈
ℝ* |
15 | | nmopub 29843 |
. . 3
⊢ (((𝑆 ∘ 𝑇): ℋ⟶ ℋ ∧
((normop‘𝑆) · (normop‘𝑇)) ∈ ℝ*)
→ ((normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))))) |
16 | 8, 14, 15 | mp2an 692 |
. 2
⊢
((normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)))) |
17 | | 0le0 11817 |
. . . . . . 7
⊢ 0 ≤
0 |
18 | 17 | a1i 11 |
. . . . . 6
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) → 0 ≤
0) |
19 | 3, 6 | lnopco0i 29939 |
. . . . . . . 8
⊢
((normop‘𝑇) = 0 → (normop‘(𝑆 ∘ 𝑇)) = 0) |
20 | 7 | nmlnop0iHIL 29931 |
. . . . . . . 8
⊢
((normop‘(𝑆 ∘ 𝑇)) = 0 ↔ (𝑆 ∘ 𝑇) = 0hop ) |
21 | 19, 20 | sylib 221 |
. . . . . . 7
⊢
((normop‘𝑇) = 0 → (𝑆 ∘ 𝑇) = 0hop ) |
22 | | fveq1 6673 |
. . . . . . . . 9
⊢ ((𝑆 ∘ 𝑇) = 0hop → ((𝑆 ∘ 𝑇)‘𝑥) = ( 0hop ‘𝑥)) |
23 | 22 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝑆 ∘ 𝑇) = 0hop →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) = (normℎ‘(
0hop ‘𝑥))) |
24 | | ho0val 29685 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℋ → (
0hop ‘𝑥) =
0ℎ) |
25 | 24 | fveq2d 6678 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ →
(normℎ‘( 0hop ‘𝑥)) =
(normℎ‘0ℎ)) |
26 | | norm0 29063 |
. . . . . . . . 9
⊢
(normℎ‘0ℎ) =
0 |
27 | 25, 26 | eqtrdi 2789 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ →
(normℎ‘( 0hop ‘𝑥)) = 0) |
28 | 23, 27 | sylan9eq 2793 |
. . . . . . 7
⊢ (((𝑆 ∘ 𝑇) = 0hop ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) = 0) |
29 | 21, 28 | sylan 583 |
. . . . . 6
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) = 0) |
30 | | oveq2 7178 |
. . . . . . . 8
⊢
((normop‘𝑇) = 0 → ((normop‘𝑆) ·
(normop‘𝑇)) = ((normop‘𝑆) · 0)) |
31 | 10 | recni 10733 |
. . . . . . . . 9
⊢
(normop‘𝑆) ∈ ℂ |
32 | 31 | mul01i 10908 |
. . . . . . . 8
⊢
((normop‘𝑆) · 0) = 0 |
33 | 30, 32 | eqtrdi 2789 |
. . . . . . 7
⊢
((normop‘𝑇) = 0 → ((normop‘𝑆) ·
(normop‘𝑇)) = 0) |
34 | 33 | adantr 484 |
. . . . . 6
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) →
((normop‘𝑆) · (normop‘𝑇)) = 0) |
35 | 18, 29, 34 | 3brtr4d 5062 |
. . . . 5
⊢
(((normop‘𝑇) = 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))) |
36 | 35 | adantrr 717 |
. . . 4
⊢
(((normop‘𝑇) = 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))) |
37 | | df-ne 2935 |
. . . . 5
⊢
((normop‘𝑇) ≠ 0 ↔ ¬
(normop‘𝑇)
= 0) |
38 | 8 | ffvelrni 6860 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝑥) ∈ ℋ) |
39 | | normcl 29060 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∘ 𝑇)‘𝑥) ∈ ℋ →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℝ) |
41 | 40 | recnd 10747 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℂ) |
42 | 12 | recni 10733 |
. . . . . . . . . . . . . 14
⊢
(normop‘𝑇) ∈ ℂ |
43 | | divrec2 11393 |
. . . . . . . . . . . . . 14
⊢
(((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℂ ∧
(normop‘𝑇)
∈ ℂ ∧ (normop‘𝑇) ≠ 0) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
44 | 42, 43 | mp3an2 1450 |
. . . . . . . . . . . . 13
⊢
(((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℂ ∧
(normop‘𝑇)
≠ 0) → ((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
45 | 41, 44 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → ((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
46 | 45 | ancoms 462 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
47 | 12 | rerecclzi 11482 |
. . . . . . . . . . . . . 14
⊢
((normop‘𝑇) ≠ 0 → (1 /
(normop‘𝑇)) ∈ ℝ) |
48 | | bdopf 29797 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶
ℋ) |
49 | 4, 48 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑇: ℋ⟶
ℋ |
50 | | nmopgt0 29847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇: ℋ⟶ ℋ →
((normop‘𝑇) ≠ 0 ↔ 0 <
(normop‘𝑇))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
((normop‘𝑇) ≠ 0 ↔ 0 <
(normop‘𝑇)) |
52 | 12 | recgt0i 11623 |
. . . . . . . . . . . . . . . 16
⊢ (0 <
(normop‘𝑇)
→ 0 < (1 / (normop‘𝑇))) |
53 | 51, 52 | sylbi 220 |
. . . . . . . . . . . . . . 15
⊢
((normop‘𝑇) ≠ 0 → 0 < (1 /
(normop‘𝑇))) |
54 | | 0re 10721 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
55 | | ltle 10807 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ (1 / (normop‘𝑇)) ∈ ℝ) → (0 < (1 /
(normop‘𝑇)) → 0 ≤ (1 /
(normop‘𝑇)))) |
56 | 54, 55 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
(normop‘𝑇)) ∈ ℝ → (0 < (1 /
(normop‘𝑇)) → 0 ≤ (1 /
(normop‘𝑇)))) |
57 | 47, 53, 56 | sylc 65 |
. . . . . . . . . . . . . 14
⊢
((normop‘𝑇) ≠ 0 → 0 ≤ (1 /
(normop‘𝑇))) |
58 | 47, 57 | absidd 14872 |
. . . . . . . . . . . . 13
⊢
((normop‘𝑇) ≠ 0 → (abs‘(1 /
(normop‘𝑇))) = (1 / (normop‘𝑇))) |
59 | 58 | adantr 484 |
. . . . . . . . . . . 12
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → (abs‘(1 /
(normop‘𝑇))) = (1 / (normop‘𝑇))) |
60 | 59 | oveq1d 7185 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥))) = ((1 / (normop‘𝑇)) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
61 | 46, 60 | eqtr4d 2776 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
62 | 42 | recclzi 11443 |
. . . . . . . . . . 11
⊢
((normop‘𝑇) ≠ 0 → (1 /
(normop‘𝑇)) ∈ ℂ) |
63 | | norm-iii 29075 |
. . . . . . . . . . 11
⊢ (((1 /
(normop‘𝑇)) ∈ ℂ ∧ ((𝑆 ∘ 𝑇)‘𝑥) ∈ ℋ) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥))) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
64 | 62, 38, 63 | syl2an 599 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥))) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)))) |
65 | 61, 64 | eqtr4d 2776 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) =
(normℎ‘((1 / (normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥)))) |
66 | 49 | ffvelrni 6860 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ) |
67 | 3 | lnopmuli 29907 |
. . . . . . . . . . . 12
⊢ (((1 /
(normop‘𝑇)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → (𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥))) = ((1 / (normop‘𝑇))
·ℎ (𝑆‘(𝑇‘𝑥)))) |
68 | 62, 66, 67 | syl2an 599 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → (𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥))) = ((1 / (normop‘𝑇))
·ℎ (𝑆‘(𝑇‘𝑥)))) |
69 | | bdopf 29797 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ BndLinOp → 𝑆: ℋ⟶
ℋ) |
70 | 1, 69 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 𝑆: ℋ⟶
ℋ |
71 | 70, 49 | hocoi 29699 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℋ → ((𝑆 ∘ 𝑇)‘𝑥) = (𝑆‘(𝑇‘𝑥))) |
72 | 71 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℋ → ((1 /
(normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥)) = ((1 / (normop‘𝑇))
·ℎ (𝑆‘(𝑇‘𝑥)))) |
73 | 72 | adantl 485 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → ((1 /
(normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥)) = ((1 / (normop‘𝑇))
·ℎ (𝑆‘(𝑇‘𝑥)))) |
74 | 68, 73 | eqtr4d 2776 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → (𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥))) = ((1 / (normop‘𝑇))
·ℎ ((𝑆 ∘ 𝑇)‘𝑥))) |
75 | 74 | fveq2d 6678 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥)))) = (normℎ‘((1 /
(normop‘𝑇)) ·ℎ
((𝑆 ∘ 𝑇)‘𝑥)))) |
76 | 65, 75 | eqtr4d 2776 |
. . . . . . . 8
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) =
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥))))) |
77 | 76 | adantrr 717 |
. . . . . . 7
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) =
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥))))) |
78 | | hvmulcl 28948 |
. . . . . . . . . 10
⊢ (((1 /
(normop‘𝑇)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) → ((1 /
(normop‘𝑇)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
79 | 62, 66, 78 | syl2an 599 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → ((1 /
(normop‘𝑇)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
80 | 79 | adantrr 717 |
. . . . . . . 8
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) → ((1 /
(normop‘𝑇)) ·ℎ (𝑇‘𝑥)) ∈ ℋ) |
81 | | norm-iii 29075 |
. . . . . . . . . . . 12
⊢ (((1 /
(normop‘𝑇)) ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘(𝑇‘𝑥)))) |
82 | 62, 66, 81 | syl2an 599 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘(𝑇‘𝑥)))) |
83 | | normcl 29060 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇‘𝑥) ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
84 | 66, 83 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
85 | 84 | recnd 10747 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℂ) |
86 | | divrec2 11393 |
. . . . . . . . . . . . . . 15
⊢
(((normℎ‘(𝑇‘𝑥)) ∈ ℂ ∧
(normop‘𝑇)
∈ ℂ ∧ (normop‘𝑇) ≠ 0) →
((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘(𝑇‘𝑥)))) |
87 | 42, 86 | mp3an2 1450 |
. . . . . . . . . . . . . 14
⊢
(((normℎ‘(𝑇‘𝑥)) ∈ ℂ ∧
(normop‘𝑇)
≠ 0) → ((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘(𝑇‘𝑥)))) |
88 | 85, 87 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → ((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘(𝑇‘𝑥)))) |
89 | 88 | ancoms 462 |
. . . . . . . . . . . 12
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) = ((1 /
(normop‘𝑇)) ·
(normℎ‘(𝑇‘𝑥)))) |
90 | 59 | oveq1d 7185 |
. . . . . . . . . . . 12
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) → ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘(𝑇‘𝑥))) = ((1 / (normop‘𝑇)) ·
(normℎ‘(𝑇‘𝑥)))) |
91 | 89, 90 | eqtr4d 2776 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) = ((abs‘(1 /
(normop‘𝑇))) ·
(normℎ‘(𝑇‘𝑥)))) |
92 | 82, 91 | eqtr4d 2776 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) = ((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇))) |
93 | 92 | adantrr 717 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) = ((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇))) |
94 | | nmoplb 29842 |
. . . . . . . . . . . . 13
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) |
95 | 49, 94 | mp3an1 1449 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) |
96 | 42 | mulid2i 10724 |
. . . . . . . . . . . 12
⊢ (1
· (normop‘𝑇)) = (normop‘𝑇) |
97 | 95, 96 | breqtrrdi 5072 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇))) |
98 | 97 | adantl 485 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇))) |
99 | 84 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → (normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
100 | | 1red 10720 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → 1 ∈ ℝ) |
101 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → (normop‘𝑇) ∈ ℝ) |
102 | 51 | biimpi 219 |
. . . . . . . . . . . . . 14
⊢
((normop‘𝑇) ≠ 0 → 0 <
(normop‘𝑇)) |
103 | 102 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → 0 < (normop‘𝑇)) |
104 | | ledivmul2 11597 |
. . . . . . . . . . . . 13
⊢
(((normℎ‘(𝑇‘𝑥)) ∈ ℝ ∧ 1 ∈ ℝ
∧ ((normop‘𝑇) ∈ ℝ ∧ 0 <
(normop‘𝑇))) →
(((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) ≤ 1 ↔
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇)))) |
105 | 99, 100, 101, 103, 104 | syl112anc 1375 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℋ ∧
(normop‘𝑇)
≠ 0) → (((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) ≤ 1 ↔
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇)))) |
106 | 105 | ancoms 462 |
. . . . . . . . . . 11
⊢
(((normop‘𝑇) ≠ 0 ∧ 𝑥 ∈ ℋ) →
(((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) ≤ 1 ↔
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇)))) |
107 | 106 | adantrr 717 |
. . . . . . . . . 10
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) ≤ 1 ↔
(normℎ‘(𝑇‘𝑥)) ≤ (1 ·
(normop‘𝑇)))) |
108 | 98, 107 | mpbird 260 |
. . . . . . . . 9
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
((normℎ‘(𝑇‘𝑥)) / (normop‘𝑇)) ≤ 1) |
109 | 93, 108 | eqbrtrd 5052 |
. . . . . . . 8
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) ≤ 1) |
110 | | nmoplb 29842 |
. . . . . . . . 9
⊢ ((𝑆: ℋ⟶ ℋ ∧
((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥)) ∈ ℋ ∧
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) ≤ 1) →
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥)))) ≤ (normop‘𝑆)) |
111 | 70, 110 | mp3an1 1449 |
. . . . . . . 8
⊢ ((((1 /
(normop‘𝑇)) ·ℎ (𝑇‘𝑥)) ∈ ℋ ∧
(normℎ‘((1 / (normop‘𝑇)) ·ℎ (𝑇‘𝑥))) ≤ 1) →
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥)))) ≤ (normop‘𝑆)) |
112 | 80, 109, 111 | syl2anc 587 |
. . . . . . 7
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘(𝑆‘((1 / (normop‘𝑇))
·ℎ (𝑇‘𝑥)))) ≤ (normop‘𝑆)) |
113 | 77, 112 | eqbrtrd 5052 |
. . . . . 6
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) ≤
(normop‘𝑆)) |
114 | 40 | ad2antrl 728 |
. . . . . . 7
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℝ) |
115 | 10 | a1i 11 |
. . . . . . 7
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normop‘𝑆)
∈ ℝ) |
116 | 102 | adantr 484 |
. . . . . . . 8
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) → 0 <
(normop‘𝑇)) |
117 | 116, 12 | jctil 523 |
. . . . . . 7
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
((normop‘𝑇) ∈ ℝ ∧ 0 <
(normop‘𝑇))) |
118 | | ledivmul2 11597 |
. . . . . . 7
⊢
(((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ∈ ℝ ∧
(normop‘𝑆)
∈ ℝ ∧ ((normop‘𝑇) ∈ ℝ ∧ 0 <
(normop‘𝑇))) →
(((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) ≤
(normop‘𝑆)
↔ (normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)))) |
119 | 114, 115,
117, 118 | syl3anc 1372 |
. . . . . 6
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(((normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) / (normop‘𝑇)) ≤
(normop‘𝑆)
↔ (normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)))) |
120 | 113, 119 | mpbid 235 |
. . . . 5
⊢
(((normop‘𝑇) ≠ 0 ∧ (𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))) |
121 | 37, 120 | sylanbr 585 |
. . . 4
⊢ ((¬
(normop‘𝑇)
= 0 ∧ (𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1)) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))) |
122 | 36, 121 | pm2.61ian 812 |
. . 3
⊢ ((𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇))) |
123 | 122 | ex 416 |
. 2
⊢ (𝑥 ∈ ℋ →
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝑆 ∘ 𝑇)‘𝑥)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)))) |
124 | 16, 123 | mprgbir 3068 |
1
⊢
(normop‘(𝑆 ∘ 𝑇)) ≤ ((normop‘𝑆) ·
(normop‘𝑇)) |