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 = HmOp U
hmoval.9 A = U adj U
Assertion hmoval U NrmCVec H = t 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 dom u adj u | u adj u t = t = t dom A | A t = t
10 df-hmo HmOp = u NrmCVec t dom u adj u | u adj u t = t
11 ovex U adj U V
12 2 11 eqeltri A V
13 12 dmex dom A V
14 13 rabex t dom A | A t = t V
15 9 10 14 fvmpt U NrmCVec HmOp U = t dom A | A t = t
16 1 15 syl5eq U NrmCVec H = t dom A | A t = t