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 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ y = A → x ⋅ ih z ⋅ ℎ y = x ⋅ ih z ⋅ ℎ A
2 1 mpteq2dv ⊢ y = A → x ∈ ℋ ⟼ x ⋅ ih z ⋅ ℎ y = x ∈ ℋ ⟼ x ⋅ ih z ⋅ ℎ A
3 oveq2 ⊢ z = B → x ⋅ ih z = x ⋅ ih B
4 3 oveq1d ⊢ z = B → x ⋅ ih z ⋅ ℎ A = x ⋅ ih B ⋅ ℎ A
5 4 mpteq2dv ⊢ z = B → x ∈ ℋ ⟼ x ⋅ ih z ⋅ ℎ A = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A
6 df-kb ⊢ ketbra = y ∈ ℋ , z ∈ ℋ ⟼ x ∈ ℋ ⟼ x ⋅ ih z ⋅ ℎ y
7 ax-hilex ⊢ ℋ ∈ V
8 7 mptex ⊢ x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A ∈ V
9 2 5 6 8 ovmpo ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A