Theorem hmoval

Description: The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hmoval.8	⊢ 𝐻 = ( HmOp ‘ 𝑈 )
	hmoval.9	⊢ 𝐴 = ( 𝑈 adj 𝑈 )
Assertion	hmoval	⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )

Proof

Step	Hyp	Ref	Expression
1		hmoval.8	⊢ 𝐻 = ( HmOp ‘ 𝑈 )
2		hmoval.9	⊢ 𝐴 = ( 𝑈 adj 𝑈 )
3		oveq12	⊢ ( ( 𝑢 = 𝑈 ∧ 𝑢 = 𝑈 ) → ( 𝑢 adj 𝑢 ) = ( 𝑈 adj 𝑈 ) )
4	3	anidms	⊢ ( 𝑢 = 𝑈 → ( 𝑢 adj 𝑢 ) = ( 𝑈 adj 𝑈 ) )
5	4 2	eqtr4di	⊢ ( 𝑢 = 𝑈 → ( 𝑢 adj 𝑢 ) = 𝐴 )
6	5	dmeqd	⊢ ( 𝑢 = 𝑈 → dom ( 𝑢 adj 𝑢 ) = dom 𝐴 )
7	5	fveq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = ( 𝐴 ‘ 𝑡 ) )
8	7	eqeq1d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 ↔ ( 𝐴 ‘ 𝑡 ) = 𝑡 ) )
9	6 8	rabeqbidv	⊢ ( 𝑢 = 𝑈 → { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )
10		df-hmo	⊢ HmOp = ( 𝑢 ∈ NrmCVec ↦ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } )
11		ovex	⊢ ( 𝑈 adj 𝑈 ) ∈ V
12	2 11	eqeltri	⊢ 𝐴 ∈ V
13	12	dmex	⊢ dom 𝐴 ∈ V
14	13	rabex	⊢ { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } ∈ V
15	9 10 14	fvmpt	⊢ ( 𝑈 ∈ NrmCVec → ( HmOp ‘ 𝑈 ) = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )
16	1 15	syl5eq	⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )