# Metamath Proof Explorer

## Theorem lnopeqi

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
Hypotheses lnopeq.1 ${⊢}{T}\in \mathrm{LinOp}$
lnopeq.2 ${⊢}{U}\in \mathrm{LinOp}$
Assertion lnopeqi ${⊢}\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}$

### Proof

Step Hyp Ref Expression
1 lnopeq.1 ${⊢}{T}\in \mathrm{LinOp}$
2 lnopeq.2 ${⊢}{U}\in \mathrm{LinOp}$
3 1 lnopfi ${⊢}{T}:ℋ⟶ℋ$
4 3 ffvelrni ${⊢}{x}\in ℋ\to {T}\left({x}\right)\in ℋ$
5 hicl ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {x}\in ℋ\right)\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\in ℂ$
6 4 5 mpancom ${⊢}{x}\in ℋ\to {T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\in ℂ$
7 2 lnopfi ${⊢}{U}:ℋ⟶ℋ$
8 7 ffvelrni ${⊢}{x}\in ℋ\to {U}\left({x}\right)\in ℋ$
9 hicl ${⊢}\left({U}\left({x}\right)\in ℋ\wedge {x}\in ℋ\right)\to {U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\in ℂ$
10 8 9 mpancom ${⊢}{x}\in ℋ\to {U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\in ℂ$
11 6 10 subeq0ad ${⊢}{x}\in ℋ\to \left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)-\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)=0↔{T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
12 hodval ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right)={T}\left({x}\right){-}_{ℎ}{U}\left({x}\right)$
13 3 7 12 mp3an12 ${⊢}{x}\in ℋ\to \left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right)={T}\left({x}\right){-}_{ℎ}{U}\left({x}\right)$
14 13 oveq1d ${⊢}{x}\in ℋ\to \left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=\left({T}\left({x}\right){-}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{x}$
15 id ${⊢}{x}\in ℋ\to {x}\in ℋ$
16 his2sub ${⊢}\left({T}\left({x}\right)\in ℋ\wedge {U}\left({x}\right)\in ℋ\wedge {x}\in ℋ\right)\to \left({T}\left({x}\right){-}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{x}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)-\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
17 4 8 15 16 syl3anc ${⊢}{x}\in ℋ\to \left({T}\left({x}\right){-}_{ℎ}{U}\left({x}\right)\right){\cdot }_{\mathrm{ih}}{x}=\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)-\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)$
18 14 17 eqtr2d ${⊢}{x}\in ℋ\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)-\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)=\left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}$
19 18 eqeq1d ${⊢}{x}\in ℋ\to \left(\left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)-\left({U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}\right)=0↔\left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\right)$
20 11 19 bitr3d ${⊢}{x}\in ℋ\to \left({T}\left({x}\right){\cdot }_{\mathrm{ih}}{x}={U}\left({x}\right){\cdot }_{\mathrm{ih}}{x}↔\left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0\right)$
21 20 ralbiia ${⊢}\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}}\left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0$
22 1 2 lnophdi ${⊢}{T}{-}_{\mathrm{op}}{U}\in \mathrm{LinOp}$
23 22 lnopeq0i ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left({T}{-}_{\mathrm{op}}{U}\right)\left({x}\right){\cdot }_{\mathrm{ih}}{x}=0↔{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}$
24 3 7 hosubeq0i ${⊢}{T}{-}_{\mathrm{op}}{U}={0}_{\mathrm{hop}}↔{T}={U}$
25 21 23 24 3bitri ${⊢}\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}$