Theorem hmop

Description: Basic inner product property of a Hermitian operator. (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmop	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B$$

Proof

Step	Hyp	Ref	Expression
1		elhmop	$$⊢T\in \mathrm{HrmOp}\leftrightarrow \left(T:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
2	1	simprbi	$$⊢T\in \mathrm{HrmOp}\to \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y$$
3	2	3ad2ant1	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y$$
4		oveq1	$$⊢x=A\to x{\cdot }_{\mathrm{ih}}T\left(y\right)=A{\cdot }_{\mathrm{ih}}T\left(y\right)$$
5		fveq2	$$⊢x=A\to T\left(x\right)=T\left(A\right)$$
6	5	oveq1d	$$⊢x=A\to T\left(x\right){\cdot }_{\mathrm{ih}}y=T\left(A\right){\cdot }_{\mathrm{ih}}y$$
7	4 6	eqeq12d	$$⊢x=A\to \left(x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow A{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(A\right){\cdot }_{\mathrm{ih}}y\right)$$
8		fveq2	$$⊢y=B\to T\left(y\right)=T\left(B\right)$$
9	8	oveq2d	$$⊢y=B\to A{\cdot }_{\mathrm{ih}}T\left(y\right)=A{\cdot }_{\mathrm{ih}}T\left(B\right)$$
10		oveq2	$$⊢y=B\to T\left(A\right){\cdot }_{\mathrm{ih}}y=T\left(A\right){\cdot }_{\mathrm{ih}}B$$
11	9 10	eqeq12d	$$⊢y=B\to \left(A{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(A\right){\cdot }_{\mathrm{ih}}y\leftrightarrow A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B\right)$$
12	7 11	rspc2v	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\to A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B\right)$$
13	12	3adant1	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}T\left(y\right)=T\left(x\right){\cdot }_{\mathrm{ih}}y\to A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B\right)$$
14	3 13	mpd	$$⊢\left(T\in \mathrm{HrmOp}\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{\cdot }_{\mathrm{ih}}T\left(B\right)=T\left(A\right){\cdot }_{\mathrm{ih}}B$$