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

Proof

Step Hyp Ref Expression
1 kbfval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A
2 1 fveq1d ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ketbra B ⁡ C = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A ⁡ C
3 oveq1 ⊢ x = C → x ⋅ ih B = C ⋅ ih B
4 3 oveq1d ⊢ x = C → x ⋅ ih B ⋅ ℎ A = C ⋅ ih B ⋅ ℎ A
5 eqid ⊢ x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A = x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A
6 ovex ⊢ C ⋅ ih B ⋅ ℎ A ∈ V
7 4 5 6 fvmpt ⊢ C ∈ ℋ → x ∈ ℋ ⟼ x ⋅ ih B ⋅ ℎ A ⁡ C = C ⋅ ih B ⋅ ℎ A
8 2 7 sylan9eq ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A
9 8 3impa ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ketbra B ⁡ C = C ⋅ ih B ⋅ ℎ A