Metamath Proof Explorer


Theorem kbfval

Description: The outer product of two vectors, expressed as | A >. <. B | in Dirac notation. See df-kb . (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

Ref Expression
Assertion kbfval ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ketbra ๐ต ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐ต ) ยทโ„Ž ๐ด ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘ฆ = ๐ด โ†’ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐‘ฆ ) = ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐ด ) )
2 1 mpteq2dv โŠข ( ๐‘ฆ = ๐ด โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐‘ฆ ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐ด ) ) )
3 oveq2 โŠข ( ๐‘ง = ๐ต โ†’ ( ๐‘ฅ ยทih ๐‘ง ) = ( ๐‘ฅ ยทih ๐ต ) )
4 3 oveq1d โŠข ( ๐‘ง = ๐ต โ†’ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐ด ) = ( ( ๐‘ฅ ยทih ๐ต ) ยทโ„Ž ๐ด ) )
5 4 mpteq2dv โŠข ( ๐‘ง = ๐ต โ†’ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐ด ) ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐ต ) ยทโ„Ž ๐ด ) ) )
6 df-kb โŠข ketbra = ( ๐‘ฆ โˆˆ โ„‹ , ๐‘ง โˆˆ โ„‹ โ†ฆ ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐‘ง ) ยทโ„Ž ๐‘ฆ ) ) )
7 ax-hilex โŠข โ„‹ โˆˆ V
8 7 mptex โŠข ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐ต ) ยทโ„Ž ๐ด ) ) โˆˆ V
9 2 5 6 8 ovmpo โŠข ( ( ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ ) โ†’ ( ๐ด ketbra ๐ต ) = ( ๐‘ฅ โˆˆ โ„‹ โ†ฆ ( ( ๐‘ฅ ยทih ๐ต ) ยทโ„Ž ๐ด ) ) )