Proof of Theorem nmcoplbi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0le0 12367 | . . . . 5
⊢ 0 ≤
0 | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝐴 = 0ℎ → 0
≤ 0) | 
| 3 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐴 = 0ℎ →
(𝑇‘𝐴) = (𝑇‘0ℎ)) | 
| 4 |  | nmcopex.1 | . . . . . . . 8
⊢ 𝑇 ∈ LinOp | 
| 5 | 4 | lnop0i 31989 | . . . . . . 7
⊢ (𝑇‘0ℎ) =
0ℎ | 
| 6 | 3, 5 | eqtrdi 2793 | . . . . . 6
⊢ (𝐴 = 0ℎ →
(𝑇‘𝐴) = 0ℎ) | 
| 7 | 6 | fveq2d 6910 | . . . . 5
⊢ (𝐴 = 0ℎ →
(normℎ‘(𝑇‘𝐴)) =
(normℎ‘0ℎ)) | 
| 8 |  | norm0 31147 | . . . . 5
⊢
(normℎ‘0ℎ) =
0 | 
| 9 | 7, 8 | eqtrdi 2793 | . . . 4
⊢ (𝐴 = 0ℎ →
(normℎ‘(𝑇‘𝐴)) = 0) | 
| 10 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐴 = 0ℎ →
(normℎ‘𝐴) =
(normℎ‘0ℎ)) | 
| 11 | 10, 8 | eqtrdi 2793 | . . . . . 6
⊢ (𝐴 = 0ℎ →
(normℎ‘𝐴) = 0) | 
| 12 | 11 | oveq2d 7447 | . . . . 5
⊢ (𝐴 = 0ℎ →
((normop‘𝑇) ·
(normℎ‘𝐴)) = ((normop‘𝑇) · 0)) | 
| 13 |  | nmcopex.2 | . . . . . . . 8
⊢ 𝑇 ∈ ContOp | 
| 14 | 4, 13 | nmcopexi 32046 | . . . . . . 7
⊢
(normop‘𝑇) ∈ ℝ | 
| 15 | 14 | recni 11275 | . . . . . 6
⊢
(normop‘𝑇) ∈ ℂ | 
| 16 | 15 | mul01i 11451 | . . . . 5
⊢
((normop‘𝑇) · 0) = 0 | 
| 17 | 12, 16 | eqtrdi 2793 | . . . 4
⊢ (𝐴 = 0ℎ →
((normop‘𝑇) ·
(normℎ‘𝐴)) = 0) | 
| 18 | 2, 9, 17 | 3brtr4d 5175 | . . 3
⊢ (𝐴 = 0ℎ →
(normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴))) | 
| 19 | 18 | adantl 481 | . 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 = 0ℎ) →
(normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴))) | 
| 20 |  | normcl 31144 | . . . . . . . . 9
⊢ (𝐴 ∈ ℋ →
(normℎ‘𝐴) ∈ ℝ) | 
| 21 | 20 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ∈ ℝ) | 
| 22 |  | normne0 31149 | . . . . . . . . 9
⊢ (𝐴 ∈ ℋ →
((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠
0ℎ)) | 
| 23 | 22 | biimpar 477 | . . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ≠ 0) | 
| 24 | 21, 23 | rereccld 12094 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (1 / (normℎ‘𝐴)) ∈ ℝ) | 
| 25 |  | normgt0 31146 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ
↔ 0 < (normℎ‘𝐴))) | 
| 26 | 25 | biimpa 476 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (normℎ‘𝐴)) | 
| 27 | 21, 26 | recgt0d 12202 | . . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (1 / (normℎ‘𝐴))) | 
| 28 |  | 0re 11263 | . . . . . . . . 9
⊢ 0 ∈
ℝ | 
| 29 |  | ltle 11349 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ (1 / (normℎ‘𝐴)) ∈ ℝ) → (0 < (1 /
(normℎ‘𝐴)) → 0 ≤ (1 /
(normℎ‘𝐴)))) | 
| 30 | 28, 29 | mpan 690 | . . . . . . . 8
⊢ ((1 /
(normℎ‘𝐴)) ∈ ℝ → (0 < (1 /
(normℎ‘𝐴)) → 0 ≤ (1 /
(normℎ‘𝐴)))) | 
| 31 | 24, 27, 30 | sylc 65 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 ≤ (1 / (normℎ‘𝐴))) | 
| 32 | 24, 31 | absidd 15461 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (abs‘(1 / (normℎ‘𝐴))) = (1 /
(normℎ‘𝐴))) | 
| 33 | 32 | oveq1d 7446 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((abs‘(1 / (normℎ‘𝐴))) ·
(normℎ‘(𝑇‘𝐴))) = ((1 /
(normℎ‘𝐴)) ·
(normℎ‘(𝑇‘𝐴)))) | 
| 34 | 24 | recnd 11289 | . . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (1 / (normℎ‘𝐴)) ∈ ℂ) | 
| 35 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 𝐴 ∈
ℋ) | 
| 36 | 4 | lnopmuli 31991 | . . . . . . . 8
⊢ (((1 /
(normℎ‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℋ) → (𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) = ((1 /
(normℎ‘𝐴)) ·ℎ (𝑇‘𝐴))) | 
| 37 | 34, 35, 36 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) = ((1 /
(normℎ‘𝐴)) ·ℎ (𝑇‘𝐴))) | 
| 38 | 37 | fveq2d 6910 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) =
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ (𝑇‘𝐴)))) | 
| 39 | 4 | lnopfi 31988 | . . . . . . . . 9
⊢ 𝑇: ℋ⟶
ℋ | 
| 40 | 39 | ffvelcdmi 7103 | . . . . . . . 8
⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ) | 
| 41 | 40 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (𝑇‘𝐴) ∈
ℋ) | 
| 42 |  | norm-iii 31159 | . . . . . . 7
⊢ (((1 /
(normℎ‘𝐴)) ∈ ℂ ∧ (𝑇‘𝐴) ∈ ℋ) →
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ (𝑇‘𝐴))) = ((abs‘(1 /
(normℎ‘𝐴))) ·
(normℎ‘(𝑇‘𝐴)))) | 
| 43 | 34, 41, 42 | syl2anc 584 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ (𝑇‘𝐴))) = ((abs‘(1 /
(normℎ‘𝐴))) ·
(normℎ‘(𝑇‘𝐴)))) | 
| 44 | 38, 43 | eqtrd 2777 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) = ((abs‘(1 /
(normℎ‘𝐴))) ·
(normℎ‘(𝑇‘𝐴)))) | 
| 45 |  | normcl 31144 | . . . . . . . . 9
⊢ ((𝑇‘𝐴) ∈ ℋ →
(normℎ‘(𝑇‘𝐴)) ∈ ℝ) | 
| 46 | 40, 45 | syl 17 | . . . . . . . 8
⊢ (𝐴 ∈ ℋ →
(normℎ‘(𝑇‘𝐴)) ∈ ℝ) | 
| 47 | 46 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘𝐴)) ∈ ℝ) | 
| 48 | 47 | recnd 11289 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘𝐴)) ∈ ℂ) | 
| 49 | 21 | recnd 11289 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘𝐴) ∈ ℂ) | 
| 50 | 48, 49, 23 | divrec2d 12047 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘(𝑇‘𝐴)) / (normℎ‘𝐴)) = ((1 /
(normℎ‘𝐴)) ·
(normℎ‘(𝑇‘𝐴)))) | 
| 51 | 33, 44, 50 | 3eqtr4rd 2788 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘(𝑇‘𝐴)) / (normℎ‘𝐴)) =
(normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)))) | 
| 52 |  | hvmulcl 31032 | . . . . . 6
⊢ (((1 /
(normℎ‘𝐴)) ∈ ℂ ∧ 𝐴 ∈ ℋ) → ((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) ∈
ℋ) | 
| 53 | 34, 35, 52 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((1 / (normℎ‘𝐴)) ·ℎ 𝐴) ∈
ℋ) | 
| 54 |  | normcl 31144 | . . . . . . 7
⊢ (((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) ∈ ℋ →
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ∈ ℝ) | 
| 55 | 53, 54 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) ∈
ℝ) | 
| 56 |  | norm1 31268 | . . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) = 1) | 
| 57 |  | eqle 11363 | . . . . . 6
⊢
(((normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) ∈ ℝ ∧
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) = 1) →
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1) | 
| 58 | 55, 56, 57 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴)) ≤ 1) | 
| 59 |  | nmoplb 31926 | . . . . . 6
⊢ ((𝑇: ℋ⟶ ℋ ∧
((1 / (normℎ‘𝐴)) ·ℎ 𝐴) ∈ ℋ ∧
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1) →
(normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) ≤
(normop‘𝑇)) | 
| 60 | 39, 59 | mp3an1 1450 | . . . . 5
⊢ ((((1 /
(normℎ‘𝐴)) ·ℎ 𝐴) ∈ ℋ ∧
(normℎ‘((1 / (normℎ‘𝐴))
·ℎ 𝐴)) ≤ 1) →
(normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) ≤
(normop‘𝑇)) | 
| 61 | 53, 58, 60 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘((1 /
(normℎ‘𝐴)) ·ℎ 𝐴))) ≤
(normop‘𝑇)) | 
| 62 | 51, 61 | eqbrtrd 5165 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ ((normℎ‘(𝑇‘𝐴)) / (normℎ‘𝐴)) ≤
(normop‘𝑇)) | 
| 63 | 14 | a1i 11 | . . . 4
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normop‘𝑇) ∈ ℝ) | 
| 64 |  | ledivmul2 12147 | . . . 4
⊢
(((normℎ‘(𝑇‘𝐴)) ∈ ℝ ∧
(normop‘𝑇)
∈ ℝ ∧ ((normℎ‘𝐴) ∈ ℝ ∧ 0 <
(normℎ‘𝐴))) →
(((normℎ‘(𝑇‘𝐴)) / (normℎ‘𝐴)) ≤
(normop‘𝑇)
↔ (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴)))) | 
| 65 | 47, 63, 21, 26, 64 | syl112anc 1376 | . . 3
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (((normℎ‘(𝑇‘𝐴)) / (normℎ‘𝐴)) ≤
(normop‘𝑇)
↔ (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴)))) | 
| 66 | 62, 65 | mpbid 232 | . 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ (normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴))) | 
| 67 | 19, 66 | pm2.61dane 3029 | 1
⊢ (𝐴 ∈ ℋ →
(normℎ‘(𝑇‘𝐴)) ≤ ((normop‘𝑇) ·
(normℎ‘𝐴))) |