Theorem cnlnadjlem4

Description: Lemma for cnlnadji . The values of auxiliary function F are vectors. (Contributed by NM, 17-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	⊢ 𝑇 ∈ LinOp
	cnlnadjlem.2	⊢ 𝑇 ∈ ContOp
	cnlnadjlem.3	⊢ 𝐺 = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·ih 𝑦 ) )
	cnlnadjlem.4	⊢ 𝐵 = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·ih 𝑦 ) = ( 𝑣 ·ih 𝑤 ) )
	cnlnadjlem.5	⊢ 𝐹 = ( 𝑦 ∈ ℋ ↦ 𝐵 )
Assertion	cnlnadjlem4	⊢ ( 𝐴 ∈ ℋ → ( 𝐹 ‘ 𝐴 ) ∈ ℋ )

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	cnlnadjlem3	⊢ ( 𝑦 ∈ ℋ → 𝐵 ∈ ℋ )
7	5 6	fmpti	⊢ 𝐹 : ℋ ⟶ ℋ
8	7	ffvelrni	⊢ ( 𝐴 ∈ ℋ → ( 𝐹 ‘ 𝐴 ) ∈ ℋ )