Metamath Proof Explorer


Theorem hommval

Description: Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion hommval ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-hilex โŠข โ„‹ โˆˆ V
2 1 1 elmap โŠข ( ๐‘‡ โˆˆ ( โ„‹ โ†‘m โ„‹ ) โ†” ๐‘‡ : โ„‹ โŸถ โ„‹ )
3 oveq1 โŠข ( ๐‘“ = ๐ด โ†’ ( ๐‘“ ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) = ( ๐ด ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) )
4 3 mpteq2dv โŠข ( ๐‘“ = ๐ด โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘“ ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) ) )
5 fveq1 โŠข ( ๐‘” = ๐‘‡ โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) = ( ๐‘‡ โ€˜ ๐‘ฅ ) )
6 5 oveq2d โŠข ( ๐‘” = ๐‘‡ โ†’ ( ๐ด ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) = ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) )
7 6 mpteq2dv โŠข ( ๐‘” = ๐‘‡ โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
8 df-homul โŠข ยทop = ( ๐‘“ โˆˆ โ„‚ , ๐‘” โˆˆ ( โ„‹ โ†‘m โ„‹ ) โ†ฆ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐‘“ ยทโ„Ž ( ๐‘” โ€˜ ๐‘ฅ ) ) ) )
9 1 mptex โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) โˆˆ V
10 4 7 8 9 ovmpo โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ โˆˆ ( โ„‹ โ†‘m โ„‹ ) ) โ†’ ( ๐ด ยทop ๐‘‡ ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )
11 2 10 sylan2br โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐‘‡ : โ„‹ โŸถ โ„‹ ) โ†’ ( ๐ด ยทop ๐‘‡ ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ๐ด ยทโ„Ž ( ๐‘‡ โ€˜ ๐‘ฅ ) ) ) )