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 ⊢T∈LinOp∧U∈LinOp→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔T=U

Proof

Step Hyp Ref Expression
1 fveq1 ⊢T=ifT∈LinOpT0hop→T⁡x=ifT∈LinOpT0hop⁡x
2 1 oveq1d ⊢T=ifT∈LinOpT0hop→T⁡x⋅ihx=ifT∈LinOpT0hop⁡x⋅ihx
3 2 eqeq1d ⊢T=ifT∈LinOpT0hop→T⁡x⋅ihx=U⁡x⋅ihx↔ifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx
4 3 ralbidv ⊢T=ifT∈LinOpT0hop→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx
5 eqeq1 ⊢T=ifT∈LinOpT0hop→T=U↔ifT∈LinOpT0hop=U
6 4 5 bibi12d ⊢T=ifT∈LinOpT0hop→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔T=U↔∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx↔ifT∈LinOpT0hop=U
7 fveq1 ⊢U=ifU∈LinOpU0hop→U⁡x=ifU∈LinOpU0hop⁡x
8 7 oveq1d ⊢U=ifU∈LinOpU0hop→U⁡x⋅ihx=ifU∈LinOpU0hop⁡x⋅ihx
9 8 eqeq2d ⊢U=ifU∈LinOpU0hop→ifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx↔ifT∈LinOpT0hop⁡x⋅ihx=ifU∈LinOpU0hop⁡x⋅ihx
10 9 ralbidv ⊢U=ifU∈LinOpU0hop→∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx↔∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=ifU∈LinOpU0hop⁡x⋅ihx
11 eqeq2 ⊢U=ifU∈LinOpU0hop→ifT∈LinOpT0hop=U↔ifT∈LinOpT0hop=ifU∈LinOpU0hop
12 10 11 bibi12d ⊢U=ifU∈LinOpU0hop→∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=U⁡x⋅ihx↔ifT∈LinOpT0hop=U↔∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=ifU∈LinOpU0hop⁡x⋅ihx↔ifT∈LinOpT0hop=ifU∈LinOpU0hop
13 0lnop ⊢0hop∈LinOp
14 13 elimel ⊢ifT∈LinOpT0hop∈LinOp
15 13 elimel ⊢ifU∈LinOpU0hop∈LinOp
16 14 15 lnopeqi ⊢∀x∈ℋifT∈LinOpT0hop⁡x⋅ihx=ifU∈LinOpU0hop⁡x⋅ihx↔ifT∈LinOpT0hop=ifU∈LinOpU0hop
17 6 12 16 dedth2h ⊢T∈LinOp∧U∈LinOp→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔T=U