This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 ∈ LinOp
cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
Assertion cnlnadjlem8 𝐹 ∈ ContOp

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 ⊢ 𝑇 ∈ LinOp
2 cnlnadjlem.2 ⊢ 𝑇 ∈ ContOp
3 cnlnadjlem.3 ⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4 cnlnadjlem.4 ⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
5 cnlnadjlem.5 ⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
6 1 2 nmcopexi ⊢ ( normop ‘ 𝑇 ) ∈ ℝ
7 1 2 3 4 5 cnlnadjlem7 ⊢ ( 𝑧 ∈ ℋ → ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) )
8 7 rgen ⊢ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) )
9 oveq1 ⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( 𝑥 · ( normℎ ‘ 𝑧 ) ) = ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) )
10 9 breq2d ⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ↔ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ) )
11 10 ralbidv ⊢ ( 𝑥 = ( normop ‘ 𝑇 ) → ( ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ) )
12 11 rspcev ⊢ ( ( ( normop ‘ 𝑇 ) ∈ ℝ ∧ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝑧 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) )
13 6 8 12 mp2an ⊢ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) )
14 1 2 3 4 5 cnlnadjlem6 ⊢ 𝐹 ∈ LinOp
15 14 lnopconi ⊢ ( 𝐹 ∈ ContOp ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ℋ ( normℎ ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 𝑥 · ( normℎ ‘ 𝑧 ) ) )
16 13 15 mpbir ⊢ 𝐹 ∈ ContOp