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 ∈ 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 eqtrid ⊢ U ∈ NrmCVec → H = t ∈ dom ⁡ A | A ⁡ t = t