Theorem hhlnoi

Description: The linear operators of Hilbert space. (Contributed by NM, 19-Nov-2007) (Revised by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlno.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhlno.2	⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
Assertion	hhlnoi	⊢ LinOp = 𝐿

Proof

Step	Hyp	Ref	Expression
1		hhlno.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhlno.2	⊢ 𝐿 = ( 𝑈 LnOp 𝑈 )
3		df-lnop	⊢ LinOp = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) }
4	1	hhnv	⊢ 𝑈 ∈ NrmCVec
5	1	hhba	⊢ ℋ = ( BaseSet ‘ 𝑈 )
6	1	hhva	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
7	1	hhsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
8	5 5 6 6 7 7 2	lnoval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑈 ∈ NrmCVec ) → 𝐿 = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) } )
9	4 4 8	mp2an	⊢ 𝐿 = { 𝑡 ∈ ( ℋ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑡 ‘ ( ( 𝑥 ·ℎ 𝑦 ) +ℎ 𝑧 ) ) = ( ( 𝑥 ·ℎ ( 𝑡 ‘ 𝑦 ) ) +ℎ ( 𝑡 ‘ 𝑧 ) ) }
10	3 9	eqtr4i	⊢ LinOp = 𝐿