# Metamath Proof Explorer

## Theorem kbval

Description: The value of the operator resulting from the outer product | A >. <. B | of two vectors. Equation 8.1 of Prugovecki p. 376. (Contributed by NM, 15-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion kbval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right)\left({C}\right)=\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}$

### Proof

Step Hyp Ref Expression
1 kbfval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}\mathrm{ketbra}{B}=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
2 1 fveq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right)\left({C}\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)\left({C}\right)$
3 oveq1 ${⊢}{x}={C}\to {x}{\cdot }_{\mathrm{ih}}{B}={C}{\cdot }_{\mathrm{ih}}{B}$
4 3 oveq1d ${⊢}{x}={C}\to \left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}=\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}$
5 eqid ${⊢}\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)$
6 ovex ${⊢}\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\in \mathrm{V}$
7 4 5 6 fvmpt ${⊢}{C}\in ℋ\to \left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}\right)\left({C}\right)=\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}$
8 2 7 sylan9eq ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge {C}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right)\left({C}\right)=\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}$
9 8 3impa ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}\mathrm{ketbra}{B}\right)\left({C}\right)=\left({C}{\cdot }_{\mathrm{ih}}{B}\right){\cdot }_{ℎ}{A}$