Metamath Proof Explorer

Theorem homcl

Description: Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion homcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({B}\right)\in ℋ$

Proof

Step Hyp Ref Expression
1 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({B}\right)={A}{\cdot }_{ℎ}{T}\left({B}\right)$
2 ffvelrn ${⊢}\left({T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to {T}\left({B}\right)\in ℋ$
3 2 anim2i ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\right)\to \left({A}\in ℂ\wedge {T}\left({B}\right)\in ℋ\right)$
4 3 3impb ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to \left({A}\in ℂ\wedge {T}\left({B}\right)\in ℋ\right)$
5 hvmulcl ${⊢}\left({A}\in ℂ\wedge {T}\left({B}\right)\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
6 4 5 syl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{T}\left({B}\right)\in ℋ$
7 1 6 eqeltrd ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {B}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({B}\right)\in ℋ$