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 | |
|
hmoval.9 | |
||
Assertion | hmoval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hmoval.8 | |
|
2 | hmoval.9 | |
|
3 | oveq12 | |
|
4 | 3 | anidms | |
5 | 4 2 | eqtr4di | |
6 | 5 | dmeqd | |
7 | 5 | fveq1d | |
8 | 7 | eqeq1d | |
9 | 6 8 | rabeqbidv | |
10 | df-hmo | |
|
11 | ovex | |
|
12 | 2 11 | eqeltri | |
13 | 12 | dmex | |
14 | 13 | rabex | |
15 | 9 10 14 | fvmpt | |
16 | 1 15 | eqtrid | |