Metamath Proof Explorer


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=HmOpU
hmoval.9 A=UadjU
Assertion hmoval UNrmCVecH=tdomA|At=t

Proof

Step Hyp Ref Expression
1 hmoval.8 H=HmOpU
2 hmoval.9 A=UadjU
3 oveq12 u=Uu=Uuadju=UadjU
4 3 anidms u=Uuadju=UadjU
5 4 2 eqtr4di u=Uuadju=A
6 5 dmeqd u=Udomuadju=domA
7 5 fveq1d u=Uuadjut=At
8 7 eqeq1d u=Uuadjut=tAt=t
9 6 8 rabeqbidv u=Utdomuadju|uadjut=t=tdomA|At=t
10 df-hmo HmOp=uNrmCVectdomuadju|uadjut=t
11 ovex UadjUV
12 2 11 eqeltri AV
13 12 dmex domAV
14 13 rabex tdomA|At=tV
15 9 10 14 fvmpt UNrmCVecHmOpU=tdomA|At=t
16 1 15 eqtrid UNrmCVecH=tdomA|At=t