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