lnfnmul

Description: Multiplicative property of a linear Hilbert space functional. (Contributed by NM, 30-May-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	lnfnmul	$⊢ (T \in LinFn \land A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B)$

Step	Hyp	Ref	Expression
1		fveq1	$⊢ T = if (T \in LinFn, T, ℋ \times \{0\}) \to T (A \cdot_{ℎ} B) = if (T \in LinFn, T, ℋ \times \{0\}) (A \cdot_{ℎ} B)$
2		fveq1	$⊢ T = if (T \in LinFn, T, ℋ \times \{0\}) \to T (B) = if (T \in LinFn, T, ℋ \times \{0\}) (B)$
3	2	oveq2d	$⊢ T = if (T \in LinFn, T, ℋ \times \{0\}) \to A T (B) = A if (T \in LinFn, T, ℋ \times \{0\}) (B)$
4	1 3	eqeq12d	$⊢ T = if (T \in LinFn, T, ℋ \times \{0\}) \to (T (A \cdot_{ℎ} B) = A T (B) \leftrightarrow if (T \in LinFn, T, ℋ \times \{0\}) (A \cdot_{ℎ} B) = A if (T \in LinFn, T, ℋ \times \{0\}) (B))$
5	4	imbi2d	$⊢ T = if (T \in LinFn, T, ℋ \times \{0\}) \to (((A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B)) \leftrightarrow ((A \in ℂ \land B \in ℋ) \to if (T \in LinFn, T, ℋ \times \{0\}) (A \cdot_{ℎ} B) = A if (T \in LinFn, T, ℋ \times \{0\}) (B)))$
6		0lnfn	$⊢ ℋ \times \{0\} \in LinFn$
7	6	elimel	$⊢ if (T \in LinFn, T, ℋ \times \{0\}) \in LinFn$
8	7	lnfnmuli	$⊢ (A \in ℂ \land B \in ℋ) \to if (T \in LinFn, T, ℋ \times \{0\}) (A \cdot_{ℎ} B) = A if (T \in LinFn, T, ℋ \times \{0\}) (B)$
9	5 8	dedth	$⊢ T \in LinFn \to ((A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B))$
10	9	3impib	$⊢ (T \in LinFn \land A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B)$

Metamath Proof Explorer