Metamath Proof Explorer

Theorem hfmmval

Description: Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	hfmmval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℂ) \to A \cdot_{fn} T = (x \in ℋ ⟼ A T (x))$

Proof

Step	Hyp	Ref	Expression
1		cnex	$⊢ ℂ \in V$
2		ax-hilex	$⊢ ℋ \in V$
3	1 2	elmap	$⊢ T \in (ℂ^{ℋ}) \leftrightarrow T : ℋ ⟶ ℂ$
4		oveq1	$⊢ f = A \to f g (x) = A g (x)$
5	4	mpteq2dv	$⊢ f = A \to (x \in ℋ ⟼ f g (x)) = (x \in ℋ ⟼ A g (x))$
6		fveq1	$⊢ g = T \to g (x) = T (x)$
7	6	oveq2d	$⊢ g = T \to A g (x) = A T (x)$
8	7	mpteq2dv	$⊢ g = T \to (x \in ℋ ⟼ A g (x)) = (x \in ℋ ⟼ A T (x))$
9		df-hfmul	$⊢ \cdot_{fn} = (f \in ℂ, g \in (ℂ^{ℋ}) ⟼ (x \in ℋ ⟼ f g (x)))$
10	2	mptex	$⊢ (x \in ℋ ⟼ A T (x)) \in V$
11	5 8 9 10	ovmpo	$⊢ (A \in ℂ \land T \in (ℂ^{ℋ})) \to A \cdot_{fn} T = (x \in ℋ ⟼ A T (x))$
12	3 11	sylan2br	$⊢ (A \in ℂ \land T : ℋ ⟶ ℂ) \to A \cdot_{fn} T = (x \in ℋ ⟼ A T (x))$