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 ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )

Proof

Step Hyp Ref Expression
1 ffvelcdm โŠข ( ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ )
2 hvmulcl โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ โ€˜ ๐‘ฅ ) โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ )
3 1 2 sylan2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ( ๐‘‡ : โ„‹ โŸถ โ„‹ โˆง ๐‘ฅ โˆˆ โ„‹ ) ) โ†’ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ )
4 3 anassrs โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โˆง ๐‘ฅ โˆˆ โ„‹ ) โ†’ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) โˆˆ โ„‹ )
5 4 fmpttd โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) : โ„‹ โŸถ โ„‹ )
6 hommval โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
7 6 feq1d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ โ†” ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) : โ„‹ โŸถ โ„‹ ) )
8 5 7 mpbird โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) : โ„‹ โŸถ โ„‹ )