Metamath Proof Explorer

Theorem lnophmi

Description: A linear operator is Hermitian if x .ih ( Tx ) takes only real values. Remark in ReedSimon p. 195. (Contributed by NM, 24-Jan-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnophm.1 ⊢ 𝑇 ∈ LinOp
lnophm.2 ⊢ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ
Assertion lnophmi 𝑇 ∈ HrmOp

Proof

Step Hyp Ref Expression
1 lnophm.1 ⊢ 𝑇 ∈ LinOp
2 lnophm.2 ⊢ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ
3 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
4 oveq1 ⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( 𝑦 ·ih ( 𝑇 ‘ 𝑧 ) ) = ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ 𝑧 ) ) )
5 fveq2 ⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) )
6 5 oveq1d ⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih 𝑧 ) )
7 4 6 eqeq12d ⊢ ( 𝑦 = if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) → ( ( 𝑦 ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ↔ ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih 𝑧 ) ) )
8 fveq2 ⊢ ( 𝑧 = if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) → ( 𝑇 ‘ 𝑧 ) = ( 𝑇 ‘ if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) )
9 8 oveq2d ⊢ ( 𝑧 = if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) → ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ 𝑧 ) ) = ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) ) )
10 oveq2 ⊢ ( 𝑧 = if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) → ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih 𝑧 ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) )
11 9 10 eqeq12d ⊢ ( 𝑧 = if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) → ( ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih 𝑧 ) ↔ ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) ) )
12 ifhvhv0 ⊢ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ∈ ℋ
13 ifhvhv0 ⊢ if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ∈ ℋ
14 12 13 1 2 lnophmlem2 ⊢ ( if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ·ih ( 𝑇 ‘ if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) ) ) = ( ( 𝑇 ‘ if ( 𝑦 ∈ ℋ , 𝑦 , 0ℎ ) ) ·ih if ( 𝑧 ∈ ℋ , 𝑧 , 0ℎ ) )
15 7 11 14 dedth2h ⊢ ( ( 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( 𝑦 ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) )
16 15 rgen2 ⊢ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑦 ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 )
17 elhmop ⊢ ( 𝑇 ∈ HrmOp ↔ ( 𝑇 : ℋ ⟶ ℋ ∧ ∀ 𝑦 ∈ ℋ ∀ 𝑧 ∈ ℋ ( 𝑦 ·ih ( 𝑇 ‘ 𝑧 ) ) = ( ( 𝑇 ‘ 𝑦 ) ·ih 𝑧 ) ) )
18 3 16 17 mpbir2an ⊢ 𝑇 ∈ HrmOp