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	|- H = ( HmOp ` U )
	hmoval.9	|- A = ( U adj U )
Assertion	hmoval	|- ( U e. NrmCVec -> H = { t e. dom A | ( A ` t ) = t } )

Proof

Step	Hyp	Ref	Expression
1		hmoval.8	|- H = ( HmOp ` U )
2		hmoval.9	|- A = ( U adj U )
3		oveq12	|- ( ( u = U /\ u = U ) -> ( u adj u ) = ( U adj U ) )
4	3	anidms	|- ( u = U -> ( u adj u ) = ( U adj U ) )
5	4 2	eqtr4di	|- ( u = U -> ( u adj u ) = A )
6	5	dmeqd	|- ( u = U -> dom ( u adj u ) = dom A )
7	5	fveq1d	|- ( u = U -> ( ( u adj u ) ` t ) = ( A ` t ) )
8	7	eqeq1d	|- ( u = U -> ( ( ( u adj u ) ` t ) = t <-> ( A ` t ) = t ) )
9	6 8	rabeqbidv	|- ( u = U -> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } = { t e. dom A | ( A ` t ) = t } )
10		df-hmo	|- HmOp = ( u e. NrmCVec |-> { t e. dom ( u adj u ) | ( ( u adj u ) ` t ) = t } )
11		ovex	|- ( U adj U ) e. _V
12	2 11	eqeltri	|- A e. _V
13	12	dmex	|- dom A e. _V
14	13	rabex	|- { t e. dom A | ( A ` t ) = t } e. _V
15	9 10 14	fvmpt	|- ( U e. NrmCVec -> ( HmOp ` U ) = { t e. dom A | ( A ` t ) = t } )
16	1 15	syl5eq	|- ( U e. NrmCVec -> H = { t e. dom A | ( A ` t ) = t } )