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 ( 𝑡 ‘ 𝑧 ) )