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