Proof of Theorem nmopub2tALT
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | normcl 31144 | . . . . . . . . . . 11
⊢ (𝑥 ∈ ℋ →
(normℎ‘𝑥) ∈ ℝ) | 
| 2 | 1 | ad2antlr 727 | . . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘𝑥) ∈ ℝ) | 
| 3 |  | simpllr 776 | . . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | 
| 4 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(normℎ‘𝑥) ≤ 1) | 
| 5 |  | 1re 11261 | . . . . . . . . . . 11
⊢ 1 ∈
ℝ | 
| 6 |  | lemul2a 12122 | . . . . . . . . . . 11
⊢
((((normℎ‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) | 
| 7 | 5, 6 | mp3anl2 1458 | . . . . . . . . . 10
⊢
((((normℎ‘𝑥) ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) | 
| 8 | 2, 3, 4, 7 | syl21anc 838 | . . . . . . . . 9
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ (𝐴 · 1)) | 
| 9 |  | ax-1rid 11225 | . . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴) | 
| 10 | 9 | ad2antrl 728 | . . . . . . . . . 10
⊢ ((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) → (𝐴 · 1) = 𝐴) | 
| 11 | 10 | ad2antrr 726 | . . . . . . . . 9
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 · 1) = 𝐴) | 
| 12 | 8, 11 | breqtrd 5169 | . . . . . . . 8
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) → (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) | 
| 13 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(𝑇‘𝑥) ∈ ℋ) | 
| 14 |  | normcl 31144 | . . . . . . . . . . . 12
⊢ ((𝑇‘𝑥) ∈ ℋ →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) | 
| 15 | 13, 14 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑥 ∈ ℋ) →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) | 
| 16 | 15 | adantlr 715 | . . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
(normℎ‘(𝑇‘𝑥)) ∈ ℝ) | 
| 17 |  | remulcl 11240 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(normℎ‘𝑥) ∈ ℝ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) | 
| 18 | 1, 17 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) | 
| 19 | 18 | adantlr 715 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) | 
| 20 | 19 | adantll 714 | . . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) → (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ) | 
| 21 |  | simplrl 777 | . . . . . . . . . 10
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) → 𝐴 ∈
ℝ) | 
| 22 |  | letr 11355 | . . . . . . . . . 10
⊢
(((normℎ‘(𝑇‘𝑥)) ∈ ℝ ∧ (𝐴 ·
(normℎ‘𝑥)) ∈ ℝ ∧ 𝐴 ∈ ℝ) →
(((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 23 | 16, 20, 21, 22 | syl3anc 1373 | . . . . . . . . 9
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
(((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
(((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) ∧ (𝐴 ·
(normℎ‘𝑥)) ≤ 𝐴) →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 25 | 12, 24 | mpan2d 694 | . . . . . . 7
⊢ ((((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) ∧
(normℎ‘𝑥) ≤ 1) →
((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 26 | 25 | ex 412 | . . . . . 6
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
((normℎ‘𝑥) ≤ 1 →
((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 27 | 26 | com23 86 | . . . . 5
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧ 𝑥 ∈ ℋ) →
((normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) →
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 28 | 27 | ralimdva 3167 | . . . 4
⊢ ((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) →
(∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥)) → ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 29 | 28 | imp 406 | . . 3
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) | 
| 30 |  | rexr 11307 | . . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) | 
| 31 | 30 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → 𝐴 ∈
ℝ*) | 
| 32 |  | nmopub 31927 | . . . . 5
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝐴 ∈
ℝ*) → ((normop‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 33 | 31, 32 | sylan2 593 | . . . 4
⊢ ((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) →
((normop‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴))) | 
| 34 | 33 | biimpar 477 | . . 3
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
((normℎ‘𝑥) ≤ 1 →
(normℎ‘(𝑇‘𝑥)) ≤ 𝐴)) → (normop‘𝑇) ≤ 𝐴) | 
| 35 | 29, 34 | syldan 591 | . 2
⊢ (((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴)) ∧
∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴) | 
| 36 | 35 | 3impa 1110 | 1
⊢ ((𝑇: ℋ⟶ ℋ ∧
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴) ∧ ∀𝑥 ∈ ℋ
(normℎ‘(𝑇‘𝑥)) ≤ (𝐴 ·
(normℎ‘𝑥))) → (normop‘𝑇) ≤ 𝐴) |