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

Metamath Proof Explorer

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	ffvelcdmi	⊢ ( 𝐴 ∈ ℋ → ( 𝐹 ‘ 𝐴 ) ∈ ℋ )