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

Metamath Proof Explorer

Theorem lnophm

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
Assertion lnophm ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → 𝑇 ∈ HrmOp )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ∈ HrmOp ↔ if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ HrmOp ) )
2 eleq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ∈ LinOp ↔ if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ) )
3 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
4 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑦 ) )
5 3 4 oveq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) = ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) )
6 5 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ↔ ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ) )
7 6 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
8 fveq1 ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑇 ‘ 𝑦 ) = ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) )
9 8 oveq2d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) )
10 9 eleq1d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ↔ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) )
11 10 ralbidv ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) )
12 7 11 bitrid ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) )
13 2 12 anbi12d ⊢ ( 𝑇 = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) ↔ ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) ) )
14 eleq1 ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( I ↾ ℋ ) ∈ LinOp ↔ if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ) )
15 fveq1 ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( I ↾ ℋ ) ‘ 𝑦 ) = ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) )
16 15 oveq2d ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) )
17 16 eleq1d ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ ↔ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) )
18 17 ralbidv ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ ↔ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) )
19 14 18 anbi12d ⊢ ( ( I ↾ ℋ ) = if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) → ( ( ( I ↾ ℋ ) ∈ LinOp ∧ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ ) ↔ ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ ) ) )
20 idlnop ⊢ ( I ↾ ℋ ) ∈ LinOp
21 fvresi ⊢ ( 𝑦 ∈ ℋ → ( ( I ↾ ℋ ) ‘ 𝑦 ) = 𝑦 )
22 21 oveq2d ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) = ( 𝑦 ·ih 𝑦 ) )
23 hiidrcl ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 ·ih 𝑦 ) ∈ ℝ )
24 22 23 eqeltrd ⊢ ( 𝑦 ∈ ℋ → ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ )
25 24 rgen ⊢ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ
26 20 25 pm3.2i ⊢ ( ( I ↾ ℋ ) ∈ LinOp ∧ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( ( I ↾ ℋ ) ‘ 𝑦 ) ) ∈ ℝ )
27 13 19 26 elimhyp ⊢ ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp ∧ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ )
28 27 simpli ⊢ if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ LinOp
29 27 simpri ⊢ ∀ 𝑦 ∈ ℋ ( 𝑦 ·ih ( if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ‘ 𝑦 ) ) ∈ ℝ
30 28 29 lnophmi ⊢ if ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) , 𝑇 , ( I ↾ ℋ ) ) ∈ HrmOp
31 1 30 dedth ⊢ ( ( 𝑇 ∈ LinOp ∧ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑥 ) ) ∈ ℝ ) → 𝑇 ∈ HrmOp )