lnfnmuli

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

		Ref	Expression
	Hypothesis	lnfnl.1	$⊢ T \in LinFn$
	Assertion	lnfnmuli	$⊢ (A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B)$

Step	Hyp	Ref	Expression
1		lnfnl.1	$⊢ T \in LinFn$
2		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
3	1	lnfnli	$⊢ (A \in ℂ \land B \in ℋ \land 0_{ℎ} \in ℋ) \to T ((A \cdot_{ℎ} B) +_{ℎ} 0_{ℎ}) = A T (B) + T (0_{ℎ})$
4	2 3	mp3an3	$⊢ (A \in ℂ \land B \in ℋ) \to T ((A \cdot_{ℎ} B) +_{ℎ} 0_{ℎ}) = A T (B) + T (0_{ℎ})$
5		hvmulcl	$⊢ (A \in ℂ \land B \in ℋ) \to A \cdot_{ℎ} B \in ℋ$
6		ax-hvaddid	$⊢ A \cdot_{ℎ} B \in ℋ \to (A \cdot_{ℎ} B) +_{ℎ} 0_{ℎ} = A \cdot_{ℎ} B$
7	5 6	syl	$⊢ (A \in ℂ \land B \in ℋ) \to (A \cdot_{ℎ} B) +_{ℎ} 0_{ℎ} = A \cdot_{ℎ} B$
8	7	fveq2d	$⊢ (A \in ℂ \land B \in ℋ) \to T ((A \cdot_{ℎ} B) +_{ℎ} 0_{ℎ}) = T (A \cdot_{ℎ} B)$
9	1	lnfn0i	$⊢ T (0_{ℎ}) = 0$
10	9	oveq2i	$⊢ A T (B) + T (0_{ℎ}) = A T (B) + 0$
11	1	lnfnfi	$⊢ T : ℋ ⟶ ℂ$
12	11	ffvelcdmi	$⊢ B \in ℋ \to T (B) \in ℂ$
13		mulcl	$⊢ (A \in ℂ \land T (B) \in ℂ) \to A T (B) \in ℂ$
14	12 13	sylan2	$⊢ (A \in ℂ \land B \in ℋ) \to A T (B) \in ℂ$
15	14	addridd	$⊢ (A \in ℂ \land B \in ℋ) \to A T (B) + 0 = A T (B)$
16	10 15	eqtrid	$⊢ (A \in ℂ \land B \in ℋ) \to A T (B) + T (0_{ℎ}) = A T (B)$
17	4 8 16	3eqtr3d	$⊢ (A \in ℂ \land B \in ℋ) \to T (A \cdot_{ℎ} B) = A T (B)$

Metamath Proof Explorer