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 ⊢ 𝐻 = ( HmOp ‘ 𝑈 )
hmoval.9 ⊢ 𝐴 = ( 𝑈 adj 𝑈 )
Assertion hmoval ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )

Proof

Step Hyp Ref Expression
1 hmoval.8 ⊢ 𝐻 = ( HmOp ‘ 𝑈 )
2 hmoval.9 ⊢ 𝐴 = ( 𝑈 adj 𝑈 )
3 oveq12 ⊢ ( ( 𝑢 = 𝑈 ∧ 𝑢 = 𝑈 ) → ( 𝑢 adj 𝑢 ) = ( 𝑈 adj 𝑈 ) )
4 3 anidms ⊢ ( 𝑢 = 𝑈 → ( 𝑢 adj 𝑢 ) = ( 𝑈 adj 𝑈 ) )
5 4 2 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( 𝑢 adj 𝑢 ) = 𝐴 )
6 5 dmeqd ⊢ ( 𝑢 = 𝑈 → dom ( 𝑢 adj 𝑢 ) = dom 𝐴 )
7 5 fveq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = ( 𝐴 ‘ 𝑡 ) )
8 7 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 ↔ ( 𝐴 ‘ 𝑡 ) = 𝑡 ) )
9 6 8 rabeqbidv ⊢ ( 𝑢 = 𝑈 → { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )
10 df-hmo ⊢ HmOp = ( 𝑢 ∈ NrmCVec ↦ { 𝑡 ∈ dom ( 𝑢 adj 𝑢 ) ∣ ( ( 𝑢 adj 𝑢 ) ‘ 𝑡 ) = 𝑡 } )
11 ovex ⊢ ( 𝑈 adj 𝑈 ) ∈ V
12 2 11 eqeltri ⊢ 𝐴 ∈ V
13 12 dmex ⊢ dom 𝐴 ∈ V
14 13 rabex ⊢ { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } ∈ V
15 9 10 14 fvmpt ⊢ ( 𝑈 ∈ NrmCVec → ( HmOp ‘ 𝑈 ) = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )
16 1 15 eqtrid ⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑡 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑡 ) = 𝑡 } )