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 \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=U\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow 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:\mathscr{H}⟶\mathscr{H}$$
4	3	ffvelrni	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
5		hicl	$$⊢\left(T\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to T\left(x\right){\cdot }_{\mathrm{ih}}x\in ℂ$$
6	4 5	mpancom	$$⊢x\in \mathscr{H}\to T\left(x\right){\cdot }_{\mathrm{ih}}x\in ℂ$$
7	2	lnopfi	$$⊢U:\mathscr{H}⟶\mathscr{H}$$
8	7	ffvelrni	$$⊢x\in \mathscr{H}\to U\left(x\right)\in \mathscr{H}$$
9		hicl	$$⊢\left(U\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to U\left(x\right){\cdot }_{\mathrm{ih}}x\in ℂ$$
10	8 9	mpancom	$$⊢x\in \mathscr{H}\to U\left(x\right){\cdot }_{\mathrm{ih}}x\in ℂ$$
11	6 10	subeq0ad	$$⊢x\in \mathscr{H}\to \left(\left(T\left(x\right){\cdot }_{\mathrm{ih}}x\right)-\left(U\left(x\right){\cdot }_{\mathrm{ih}}x\right)=0\leftrightarrow T\left(x\right){\cdot }_{\mathrm{ih}}x=U\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
12		hodval	$$⊢\left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\wedge x\in \mathscr{H}\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 \mathscr{H}\to \left(T{-}_{\mathrm{op}}U\right)\left(x\right)=T\left(x\right){-}_{ℎ}U\left(x\right)$$
14	13	oveq1d	$$⊢x\in \mathscr{H}\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 \mathscr{H}\to x\in \mathscr{H}$$
16		his2sub	$$⊢\left(T\left(x\right)\in \mathscr{H}\wedge U\left(x\right)\in \mathscr{H}\wedge x\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\to \left(\left(T\left(x\right){\cdot }_{\mathrm{ih}}x\right)-\left(U\left(x\right){\cdot }_{\mathrm{ih}}x\right)=0\leftrightarrow \left(T{-}_{\mathrm{op}}U\right)\left(x\right){\cdot }_{\mathrm{ih}}x=0\right)$$
20	11 19	bitr3d	$$⊢x\in \mathscr{H}\to \left(T\left(x\right){\cdot }_{\mathrm{ih}}x=U\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow \left(T{-}_{\mathrm{op}}U\right)\left(x\right){\cdot }_{\mathrm{ih}}x=0\right)$$
21	20	ralbiia	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=U\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow \forall x\in \mathscr{H}\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 \mathscr{H}\left(T{-}_{\mathrm{op}}U\right)\left(x\right){\cdot }_{\mathrm{ih}}x=0\leftrightarrow T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}$$
24	3 7	hosubeq0i	$$⊢T{-}_{\mathrm{op}}U=0_{\mathrm{hop}}\leftrightarrow T=U$$
25	21 23 24	3bitri	$$⊢\forall x\in \mathscr{H}T\left(x\right){\cdot }_{\mathrm{ih}}x=U\left(x\right){\cdot }_{\mathrm{ih}}x\leftrightarrow T=U$$