Theorem cnlnadjlem3

Description: Lemma for cnlnadji . By riesz4 , B is the unique vector such that ( Tv ) .ih y ) = ( v .ih w ) for all v . (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 𝑤 ) )
Assertion	cnlnadjlem3	⊢ ( 𝑦 ∈ ℋ → 𝐵 ∈ ℋ )

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	⊢ 𝑇 ∈ LinOp
2		cnlnadjlem.2	⊢ 𝑇 ∈ ContOp
3		cnlnadjlem.3	⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
4		cnlnadjlem.4	⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
5	1 2 3	cnlnadjlem2	⊢ ( 𝑦 ∈ ℋ → ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )
6		elin	⊢ ( 𝐺 ∈ ( LinFn ∩ ContFn ) ↔ ( 𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn ) )
7	5 6	sylibr	⊢ ( 𝑦 ∈ ℋ → 𝐺 ∈ ( LinFn ∩ ContFn ) )
8		riesz4	⊢ ( 𝐺 ∈ ( LinFn ∩ ContFn ) → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝐺 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
9	7 8	syl	⊢ ( 𝑦 ∈ ℋ → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝐺 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) )
10	1 2 3	cnlnadjlem1	⊢ ( 𝑣 ∈ ℋ → ( 𝐺 ‘ 𝑣 ) = ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) )
11	10	eqeq1d	⊢ ( 𝑣 ∈ ℋ → ( ( 𝐺 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ) )
12	11	ralbiia	⊢ ( ∀ 𝑣 ∈ ℋ ( 𝐺 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
13	12	reubii	⊢ ( ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( 𝐺 ‘ 𝑣 ) = ( 𝑣 ·ih 𝑤 ) ↔ ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
14	9 13	sylib	⊢ ( 𝑦 ∈ ℋ → ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
15		riotacl	⊢ ( ∃! 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) → ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ) ∈ ℋ )
16	14 15	syl	⊢ ( 𝑦 ∈ ℋ → ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) ) ∈ ℋ )
17	4 16	eqeltrid	⊢ ( 𝑦 ∈ ℋ → 𝐵 ∈ ℋ )