This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 eqtrid 
 |-  ( U e. NrmCVec -> H = { t e. dom A | ( A ` t ) = t } )