# 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 𝑥 ) ↔ 𝑇 = 𝑈 ) )