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

Metamath Proof Explorer

Theorem cnlnadjlem9

Description: Lemma for cnlnadji . F provides an example showing the existence of a continuous linear adjoint. (Contributed by NM, 18-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 cnlnadjlem9 ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) )

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 3 4 5 cnlnadjlem6 ⊢ 𝐹 ∈ LinOp
7 1 2 3 4 5 cnlnadjlem8 ⊢ 𝐹 ∈ ContOp
8 elin ⊢ ( 𝐹 ∈ ( LinOp ∩ ContOp ) ↔ ( 𝐹 ∈ LinOp ∧ 𝐹 ∈ ContOp ) )
9 6 7 8 mpbir2an ⊢ 𝐹 ∈ ( LinOp ∩ ContOp )
10 1 2 3 4 5 cnlnadjlem5 ⊢ ( ( 𝑧 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) )
11 10 ancoms ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) )
12 11 rgen2 ⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) )
13 fveq1 ⊢ ( 𝑡 = 𝐹 → ( 𝑡 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
14 13 oveq2d ⊢ ( 𝑡 = 𝐹 → ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) )
15 14 eqeq2d ⊢ ( 𝑡 = 𝐹 → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) ) )
16 15 2ralbidv ⊢ ( 𝑡 = 𝐹 → ( ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) ) )
17 16 rspcev ⊢ ( ( 𝐹 ∈ ( LinOp ∩ ContOp ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝐹 ‘ 𝑧 ) ) ) → ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) ) )
18 9 12 17 mp2an ⊢ ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑧 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑧 ) = ( 𝑥 ·ih ( 𝑡 ‘ 𝑧 ) )