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

Metamath Proof Explorer

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 = 𝐿