Step | Hyp | Ref
| Expression |
1 | | nmophm.1 |
. . . . . . . . . . 11
⊢ 𝑇 ∈
BndLinOp |
2 | | bdopf 29797 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ BndLinOp → 𝑇: ℋ⟶
ℋ) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑇: ℋ⟶
ℋ |
4 | | homval 29676 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
((𝐴
·op 𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
5 | 3, 4 | mp3an2 1450 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) → ((𝐴 ·op
𝑇)‘𝑥) = (𝐴 ·ℎ (𝑇‘𝑥))) |
6 | 5 | fveq2d 6679 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) = (normℎ‘(𝐴
·ℎ (𝑇‘𝑥)))) |
7 | 3 | ffvelrni 6861 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℋ → (𝑇‘𝑥) ∈ ℋ) |
8 | | norm-iii 29075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ (𝑇‘𝑥) ∈ ℋ) →
(normℎ‘(𝐴 ·ℎ (𝑇‘𝑥))) = ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥)))) |
9 | 7, 8 | sylan2 596 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝐴 ·ℎ (𝑇‘𝑥))) = ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥)))) |
10 | 6, 9 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) = ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥)))) |
11 | 10 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) = ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥)))) |
12 | | normcl 29060 |
. . . . . . . . 9
⊢ ((𝑇‘𝑥) ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
13 | 7, 12 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
14 | 13 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
15 | | abscl 14729 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
16 | | absge0 14738 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
17 | 15, 16 | jca 515 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) |
18 | 17 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
19 | | nmoplb 29842 |
. . . . . . . . 9
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) |
20 | 3, 19 | mp3an1 1449 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) |
21 | 20 | adantll 714 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) |
22 | | nmopre 29805 |
. . . . . . . . 9
⊢ (𝑇 ∈ BndLinOp →
(normop‘𝑇)
∈ ℝ) |
23 | 1, 22 | ax-mp 5 |
. . . . . . . 8
⊢
(normop‘𝑇) ∈ ℝ |
24 | | lemul2a 11574 |
. . . . . . . 8
⊢
((((normℎ‘(𝑇‘𝑥)) ∈ ℝ ∧
(normop‘𝑇)
∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) ∧
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) → ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ ((abs‘𝐴) · (normop‘𝑇))) |
25 | 23, 24 | mp3anl2 1457 |
. . . . . . 7
⊢
((((normℎ‘(𝑇‘𝑥)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) ∧
(normℎ‘(𝑇‘𝑥)) ≤ (normop‘𝑇)) → ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ ((abs‘𝐴) · (normop‘𝑇))) |
26 | 14, 18, 21, 25 | syl21anc 837 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ ((abs‘𝐴) · (normop‘𝑇))) |
27 | 11, 26 | eqbrtrd 5053 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ ((abs‘𝐴) · (normop‘𝑇))) |
28 | 27 | ex 416 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) →
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ ((abs‘𝐴) · (normop‘𝑇)))) |
29 | 28 | ralrimiva 3096 |
. . 3
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ ((abs‘𝐴) · (normop‘𝑇)))) |
30 | | homulcl 29694 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ)
→ (𝐴
·op 𝑇): ℋ⟶ ℋ) |
31 | 3, 30 | mpan2 691 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 ·op
𝑇): ℋ⟶
ℋ) |
32 | | remulcl 10701 |
. . . . . 6
⊢
(((abs‘𝐴)
∈ ℝ ∧ (normop‘𝑇) ∈ ℝ) → ((abs‘𝐴) ·
(normop‘𝑇)) ∈ ℝ) |
33 | 15, 23, 32 | sylancl 589 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ·
(normop‘𝑇)) ∈ ℝ) |
34 | 33 | rexrd 10770 |
. . . 4
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ·
(normop‘𝑇)) ∈
ℝ*) |
35 | | nmopub 29843 |
. . . 4
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ ((abs‘𝐴)
· (normop‘𝑇)) ∈ ℝ*) →
((normop‘(𝐴 ·op 𝑇)) ≤ ((abs‘𝐴) ·
(normop‘𝑇)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ ((abs‘𝐴) · (normop‘𝑇))))) |
36 | 31, 34, 35 | syl2anc 587 |
. . 3
⊢ (𝐴 ∈ ℂ →
((normop‘(𝐴 ·op 𝑇)) ≤ ((abs‘𝐴) ·
(normop‘𝑇)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ ((abs‘𝐴) · (normop‘𝑇))))) |
37 | 29, 36 | mpbird 260 |
. 2
⊢ (𝐴 ∈ ℂ →
(normop‘(𝐴
·op 𝑇)) ≤ ((abs‘𝐴) · (normop‘𝑇))) |
38 | | fveq2 6675 |
. . . . . . . 8
⊢ (𝐴 = 0 → (abs‘𝐴) =
(abs‘0)) |
39 | | abs0 14736 |
. . . . . . . 8
⊢
(abs‘0) = 0 |
40 | 38, 39 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝐴 = 0 → (abs‘𝐴) = 0) |
41 | 40 | oveq1d 7186 |
. . . . . 6
⊢ (𝐴 = 0 → ((abs‘𝐴) ·
(normop‘𝑇)) = (0 ·
(normop‘𝑇))) |
42 | 23 | recni 10734 |
. . . . . . 7
⊢
(normop‘𝑇) ∈ ℂ |
43 | 42 | mul02i 10908 |
. . . . . 6
⊢ (0
· (normop‘𝑇)) = 0 |
44 | 41, 43 | eqtrdi 2789 |
. . . . 5
⊢ (𝐴 = 0 → ((abs‘𝐴) ·
(normop‘𝑇)) = 0) |
45 | 44 | adantl 485 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 = 0) → ((abs‘𝐴) ·
(normop‘𝑇)) = 0) |
46 | | nmopge0 29846 |
. . . . . 6
⊢ ((𝐴 ·op
𝑇): ℋ⟶ ℋ
→ 0 ≤ (normop‘(𝐴 ·op 𝑇))) |
47 | 31, 46 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 0 ≤
(normop‘(𝐴
·op 𝑇))) |
48 | 47 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 = 0) → 0 ≤
(normop‘(𝐴
·op 𝑇))) |
49 | 45, 48 | eqbrtrd 5053 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 = 0) → ((abs‘𝐴) ·
(normop‘𝑇)) ≤ (normop‘(𝐴 ·op
𝑇))) |
50 | | nmoplb 29842 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·op
𝑇): ℋ⟶ ℋ
∧ 𝑥 ∈ ℋ
∧ (normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ (normop‘(𝐴 ·op
𝑇))) |
51 | 31, 50 | syl3an1 1164 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ (normop‘(𝐴 ·op
𝑇))) |
52 | 51 | 3expa 1119 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘((𝐴 ·op 𝑇)‘𝑥)) ≤ (normop‘(𝐴 ·op
𝑇))) |
53 | 11, 52 | eqbrtrrd 5055 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ (normop‘(𝐴 ·op
𝑇))) |
54 | 53 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → ((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ (normop‘(𝐴 ·op
𝑇))) |
55 | 13 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) |
56 | | nmopxr 29801 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ·op
𝑇): ℋ⟶ ℋ
→ (normop‘(𝐴 ·op 𝑇)) ∈
ℝ*) |
57 | 31, 56 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ →
(normop‘(𝐴
·op 𝑇)) ∈
ℝ*) |
58 | | nmopgtmnf 29803 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ·op
𝑇): ℋ⟶ ℋ
→ -∞ < (normop‘(𝐴 ·op 𝑇))) |
59 | 31, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → -∞
< (normop‘(𝐴 ·op 𝑇))) |
60 | | xrre 12646 |
. . . . . . . . . . . 12
⊢
((((normop‘(𝐴 ·op 𝑇)) ∈ ℝ*
∧ ((abs‘𝐴)
· (normop‘𝑇)) ∈ ℝ) ∧ (-∞ <
(normop‘(𝐴
·op 𝑇)) ∧ (normop‘(𝐴 ·op
𝑇)) ≤ ((abs‘𝐴) ·
(normop‘𝑇)))) → (normop‘(𝐴 ·op
𝑇)) ∈
ℝ) |
61 | 57, 33, 59, 37, 60 | syl22anc 838 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ →
(normop‘(𝐴
·op 𝑇)) ∈ ℝ) |
62 | 61 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) →
(normop‘(𝐴
·op 𝑇)) ∈ ℝ) |
63 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) →
(abs‘𝐴) ∈
ℝ) |
64 | | absgt0 14775 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 ≠ 0 ↔ 0 <
(abs‘𝐴))) |
65 | 64 | biimpa 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 0 <
(abs‘𝐴)) |
66 | 65 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) → 0 <
(abs‘𝐴)) |
67 | | lemuldiv2 11600 |
. . . . . . . . . 10
⊢
(((normℎ‘(𝑇‘𝑥)) ∈ ℝ ∧
(normop‘(𝐴
·op 𝑇)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 <
(abs‘𝐴))) →
(((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ (normop‘(𝐴 ·op
𝑇)) ↔
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)))) |
68 | 55, 62, 63, 66, 67 | syl112anc 1375 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) →
(((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ (normop‘(𝐴 ·op
𝑇)) ↔
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)))) |
69 | 68 | adantr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (((abs‘𝐴) ·
(normℎ‘(𝑇‘𝑥))) ≤ (normop‘(𝐴 ·op
𝑇)) ↔
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)))) |
70 | 54, 69 | mpbid 235 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴))) |
71 | 70 | ex 416 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝑥 ∈ ℋ) →
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)))) |
72 | 71 | ralrimiva 3096 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)))) |
73 | 61 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(normop‘(𝐴
·op 𝑇)) ∈ ℝ) |
74 | 15 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ) |
75 | | abs00 14740 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) = 0 ↔
𝐴 = 0)) |
76 | 75 | necon3bid 2978 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ≠ 0
↔ 𝐴 ≠
0)) |
77 | 76 | biimpar 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ≠ 0) |
78 | 73, 74, 77 | redivcld 11547 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴)) ∈
ℝ) |
79 | 78 | rexrd 10770 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴)) ∈
ℝ*) |
80 | | nmopub 29843 |
. . . . . 6
⊢ ((𝑇: ℋ⟶ ℋ ∧
((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴)) ∈ ℝ*)
→ ((normop‘𝑇) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴))))) |
81 | 3, 79, 80 | sylancr 590 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((normop‘𝑇) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴)) ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ ((normop‘(𝐴 ·op
𝑇)) / (abs‘𝐴))))) |
82 | 72, 81 | mpbird 260 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(normop‘𝑇)
≤ ((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴))) |
83 | 23 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(normop‘𝑇)
∈ ℝ) |
84 | | lemuldiv2 11600 |
. . . . 5
⊢
(((normop‘𝑇) ∈ ℝ ∧
(normop‘(𝐴
·op 𝑇)) ∈ ℝ ∧ ((abs‘𝐴) ∈ ℝ ∧ 0 <
(abs‘𝐴))) →
(((abs‘𝐴) ·
(normop‘𝑇)) ≤ (normop‘(𝐴 ·op
𝑇)) ↔
(normop‘𝑇)
≤ ((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴)))) |
85 | 83, 73, 74, 65, 84 | syl112anc 1375 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
(((abs‘𝐴) ·
(normop‘𝑇)) ≤ (normop‘(𝐴 ·op
𝑇)) ↔
(normop‘𝑇)
≤ ((normop‘(𝐴 ·op 𝑇)) / (abs‘𝐴)))) |
86 | 82, 85 | mpbird 260 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) →
((abs‘𝐴) ·
(normop‘𝑇)) ≤ (normop‘(𝐴 ·op
𝑇))) |
87 | 49, 86 | pm2.61dane 3021 |
. 2
⊢ (𝐴 ∈ ℂ →
((abs‘𝐴) ·
(normop‘𝑇)) ≤ (normop‘(𝐴 ·op
𝑇))) |
88 | 61, 33 | letri3d 10861 |
. 2
⊢ (𝐴 ∈ ℂ →
((normop‘(𝐴 ·op 𝑇)) = ((abs‘𝐴) ·
(normop‘𝑇)) ↔ ((normop‘(𝐴 ·op
𝑇)) ≤ ((abs‘𝐴) ·
(normop‘𝑇)) ∧ ((abs‘𝐴) · (normop‘𝑇)) ≤
(normop‘(𝐴
·op 𝑇))))) |
89 | 37, 87, 88 | mpbir2and 713 |
1
⊢ (𝐴 ∈ ℂ →
(normop‘(𝐴
·op 𝑇)) = ((abs‘𝐴) · (normop‘𝑇))) |