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∈ℋ→AketbraB⁡C=C⋅ihB⋅ℎA

Proof

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