Metamath Proof Explorer


Theorem homulcl

Description: The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion homulcl AT:A·opT:

Proof

Step Hyp Ref Expression
1 ffvelcdm T:xTx
2 hvmulcl ATxATx
3 1 2 sylan2 AT:xATx
4 3 anassrs AT:xATx
5 4 fmpttd AT:xATx:
6 hommval AT:A·opT=xATx
7 6 feq1d AT:A·opT:xATx:
8 5 7 mpbird AT:A·opT: