# Metamath Proof Explorer

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

Ref Expression
cnlnadjlem.3 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇𝑔 ) ·ih 𝑦 ) )
cnlnadjlem.4 𝐵 = ( 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
cnlnadjlem.5 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )

### Proof

Step Hyp Ref Expression
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