# 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 ${⊢}\left({T}\in \mathrm{LinOp}\wedge {U}\in \mathrm{LinOp}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔{T}={U}\right)$

### Proof

Step Hyp Ref Expression
1 fveq1 ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to {T}\left({x}\right)=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right)$
2 1 oveq1d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
3 2 eqeq1d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
4 3 ralbidv ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
5 eqeq1 ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to \left({T}={U}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)={U}\right)$
6 4 5 bibi12d ${⊢}{T}=if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\to \left(\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔{T}={U}\right)↔\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)={U}\right)\right)$
7 fveq1 ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to {U}\left({x}\right)=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right)$
8 7 oveq1d ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to {U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
9 8 eqeq2d ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to \left(if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
10 9 ralbidv ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
11 eqeq2 ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to \left(if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)={U}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\right)$
12 10 11 bibi12d ${⊢}{U}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\to \left(\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)={U}\right)↔\left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\right)\right)$
13 0lnop ${⊢}{0}_{\mathrm{hop}}\in \mathrm{LinOp}$
14 13 elimel ${⊢}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\in \mathrm{LinOp}$
15 13 elimel ${⊢}if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\in \mathrm{LinOp}$
16 14 15 lnopeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔if\left({T}\in \mathrm{LinOp},{T},{0}_{\mathrm{hop}}\right)=if\left({U}\in \mathrm{LinOp},{U},{0}_{\mathrm{hop}}\right)$
17 6 12 16 dedth2h ${⊢}\left({T}\in \mathrm{LinOp}\wedge {U}\in \mathrm{LinOp}\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔{T}={U}\right)$