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=\mathrm{HmOp}\left(U\right)$$
	hmoval.9	$$⊢A=U\mathrm{adj}U$$
Assertion	hmoval	$$⊢U\in \mathrm{NrmCVec}\to H=\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}$$

Proof

Step	Hyp	Ref	Expression
1		hmoval.8	$$⊢H=\mathrm{HmOp}\left(U\right)$$
2		hmoval.9	$$⊢A=U\mathrm{adj}U$$
3		oveq12	$$⊢\left(u=U\wedge u=U\right)\to u\mathrm{adj}u=U\mathrm{adj}U$$
4	3	anidms	$$⊢u=U\to u\mathrm{adj}u=U\mathrm{adj}U$$
5	4 2	eqtr4di	$$⊢u=U\to u\mathrm{adj}u=A$$
6	5	dmeqd	$$⊢u=U\to \mathrm{dom}\left(u\mathrm{adj}u\right)=\mathrm{dom}A$$
7	5	fveq1d	$$⊢u=U\to \left(u\mathrm{adj}u\right)\left(t\right)=A\left(t\right)$$
8	7	eqeq1d	$$⊢u=U\to \left(\left(u\mathrm{adj}u\right)\left(t\right)=t\leftrightarrow A\left(t\right)=t\right)$$
9	6 8	rabeqbidv	$$⊢u=U\to \left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}=\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}$$
10		df-hmo	$$⊢\mathrm{HmOp}=\left(u\in \mathrm{NrmCVec}⟼\left\{t\in \mathrm{dom}\left(u\mathrm{adj}u\right)|\left(u\mathrm{adj}u\right)\left(t\right)=t\right\}\right)$$
11		ovex	$$⊢U\mathrm{adj}U\in \mathrm{V}$$
12	2 11	eqeltri	$$⊢A\in \mathrm{V}$$
13	12	dmex	$$⊢\mathrm{dom}A\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}\in \mathrm{V}$$
15	9 10 14	fvmpt	$$⊢U\in \mathrm{NrmCVec}\to \mathrm{HmOp}\left(U\right)=\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}$$
16	1 15	eqtrid	$$⊢U\in \mathrm{NrmCVec}\to H=\left\{t\in \mathrm{dom}A|A\left(t\right)=t\right\}$$