df-hmo

Description: Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-hmo	⊢ HmOp = ( 𝑢 ∈ NrmCVec ↦ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chmo	⊢ HmOp
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vt	⊢ 𝑡
4	1	cv	⊢ 𝑢
5		caj	⊢ adj
6	4 4 5	co	⊢ ( 𝑢 adj 𝑢 )
7	6	cdm	⊢ dom ( 𝑢 adj 𝑢 )
8	3	cv	⊢ 𝑡
9	8 6	cfv	⊢ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 )
10	9 8	wceq	⊢ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡
11	10 3 7	crab	⊢ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 }
12	1 2 11	cmpt	⊢ ( 𝑢 ∈ NrmCVec ↦ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } )
13	0 12	wceq	⊢ HmOp = ( 𝑢 ∈ NrmCVec ↦ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } )

Metamath Proof Explorer

Definition df-hmo

Detailed syntax breakdown