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

Metamath Proof Explorer

Theorem lnopeqi

Description: Two linear Hilbert space operators are equal iff their quadratic forms are equal. (Contributed by NM, 27-Jul-2006) (New usage is discouraged.)

Ref Expression
Hypotheses lnopeq.1 ⊢ 𝑇 ∈ LinOp
lnopeq.2 ⊢ 𝑈 ∈ LinOp
Assertion lnopeqi ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝑇 = 𝑈 )

Proof

Step Hyp Ref Expression
1 lnopeq.1 ⊢ 𝑇 ∈ LinOp
2 lnopeq.2 ⊢ 𝑈 ∈ LinOp
3 1 lnopfi ⊢ 𝑇 : ℋ ⟶ ℋ
4 3 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
5 hicl ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℂ )
6 4 5 mpancom ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℂ )
7 2 lnopfi ⊢ 𝑈 : ℋ ⟶ ℋ
8 7 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
9 hicl ⊢ ( ( ( 𝑈 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℂ )
10 8 9 mpancom ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℂ )
11 6 10 subeq0ad ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) = 0 ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
12 hodval ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) −ℎ ( 𝑈 ‘ 𝑥 ) ) )
13 3 7 12 mp3an12 ⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) −ℎ ( 𝑈 ‘ 𝑥 ) ) )
14 13 oveq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) −ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) )
15 id ⊢ ( 𝑥 ∈ ℋ → 𝑥 ∈ ℋ )
16 his2sub ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑈 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑥 ) −ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
17 4 8 15 16 syl3anc ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑇 ‘ 𝑥 ) −ℎ ( 𝑈 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
18 14 17 eqtr2d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) = ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) )
19 18 eqeq1d ⊢ ( 𝑥 ∈ ℋ → ( ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) = 0 ↔ ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = 0 ) )
20 11 19 bitr3d ⊢ ( 𝑥 ∈ ℋ → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = 0 ) )
21 20 ralbiia ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = 0 )
22 1 2 lnophdi ⊢ ( 𝑇 −op 𝑈 ) ∈ LinOp
23 22 lnopeq0i ⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( 𝑇 −op 𝑈 ) ‘ 𝑥 ) ·ih 𝑥 ) = 0 ↔ ( 𝑇 −op 𝑈 ) = 0hop )
24 3 7 hosubeq0i ⊢ ( ( 𝑇 −op 𝑈 ) = 0hop ↔ 𝑇 = 𝑈 )
25 21 23 24 3bitri ⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝑇 = 𝑈 )