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

Metamath Proof Explorer

Theorem lnopeq

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
Assertion lnopeq ( ( 𝑇 ∈ LinOp ∧ 𝑈 ∈ LinOp ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝑇 = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( 𝑇 ‘ 𝑥 ) = ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) )
2 1 oveq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) )
3 2 eqeq1d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
4 3 ralbidv ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
5 eqeq1 ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( 𝑇 = 𝑈 ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 𝑈 ) )
6 4 5 bibi12d ⊢ ( 𝑇 = if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) → ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝑇 = 𝑈 ) ↔ ( ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 𝑈 ) ) )
7 fveq1 ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( 𝑈 ‘ 𝑥 ) = ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) )
8 7 oveq1d ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) )
9 8 eqeq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
10 9 ralbidv ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
11 eqeq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 𝑈 ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ) )
12 10 11 bibi12d ⊢ ( 𝑈 = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) → ( ( ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = 𝑈 ) ↔ ( ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ) ) )
13 0lnop ⊢ 0hop ∈ LinOp
14 13 elimel ⊢ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ∈ LinOp
15 13 elimel ⊢ if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ∈ LinOp
16 14 15 lnopeqi ⊢ ( ∀ 𝑥 ∈ ℋ ( ( if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ if ( 𝑇 ∈ LinOp , 𝑇 , 0hop ) = if ( 𝑈 ∈ LinOp , 𝑈 , 0hop ) )
17 6 12 16 dedth2h ⊢ ( ( 𝑇 ∈ LinOp ∧ 𝑈 ∈ LinOp ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ↔ 𝑇 = 𝑈 ) )