Metamath Proof Explorer


Theorem hococli

Description: Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses hoeq.1 S:
hoeq.2 T:
Assertion hococli ASTA

Proof

Step Hyp Ref Expression
1 hoeq.1 S:
2 hoeq.2 T:
3 1 2 hocoi ASTA=STA
4 2 ffvelrni ATA
5 1 ffvelrni TASTA
6 4 5 syl ASTA
7 3 6 eqeltrd ASTA