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	syl5bb	⊢ ( 𝑇 = 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 )