Metamath Proof Explorer

Theorem cnlnadjlem8

Description: Lemma for cnlnadji . F is continuous. (Contributed by NM, 17-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 ⊢ T ∈ LinOp
cnlnadjlem.2 ⊢ T ∈ ContOp
cnlnadjlem.3 ⊢ G = g ∈ ℋ ⟼ T ⁡ g ⋅ ih y
cnlnadjlem.4 ⊢ B = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
cnlnadjlem.5 ⊢ F = y ∈ ℋ ⟼ B
Assertion cnlnadjlem8 ⊢ F ∈ ContOp

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ T ∈ LinOp
2 cnlnadjlem.2 ⊢ T ∈ ContOp
3 cnlnadjlem.3 ⊢ G = g ∈ ℋ ⟼ T ⁡ g ⋅ ih y
4 cnlnadjlem.4 ⊢ B = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih y = v ⋅ ih w
5 cnlnadjlem.5 ⊢ F = y ∈ ℋ ⟼ B
6 1 2 nmcopexi ⊢ norm op ⁡ T ∈ ℝ
7 1 2 3 4 5 cnlnadjlem7 ⊢ z ∈ ℋ → norm ℎ ⁡ F ⁡ z ≤ norm op ⁡ T ⁢ norm ℎ ⁡ z
8 7 rgen ⊢ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ norm op ⁡ T ⁢ norm ℎ ⁡ z
9 oveq1 ⊢ x = norm op ⁡ T → x ⁢ norm ℎ ⁡ z = norm op ⁡ T ⁢ norm ℎ ⁡ z
10 9 breq2d ⊢ x = norm op ⁡ T → norm ℎ ⁡ F ⁡ z ≤ x ⁢ norm ℎ ⁡ z ↔ norm ℎ ⁡ F ⁡ z ≤ norm op ⁡ T ⁢ norm ℎ ⁡ z
11 10 ralbidv ⊢ x = norm op ⁡ T → ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ x ⁢ norm ℎ ⁡ z ↔ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ norm op ⁡ T ⁢ norm ℎ ⁡ z
12 11 rspcev ⊢ norm op ⁡ T ∈ ℝ ∧ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ norm op ⁡ T ⁢ norm ℎ ⁡ z → ∃ x ∈ ℝ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ x ⁢ norm ℎ ⁡ z
13 6 8 12 mp2an ⊢ ∃ x ∈ ℝ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ x ⁢ norm ℎ ⁡ z
14 1 2 3 4 5 cnlnadjlem6 ⊢ F ∈ LinOp
15 14 lnopconi ⊢ F ∈ ContOp ↔ ∃ x ∈ ℝ ∀ z ∈ ℋ norm ℎ ⁡ F ⁡ z ≤ x ⁢ norm ℎ ⁡ z
16 13 15 mpbir ⊢ F ∈ ContOp