Metamath Proof Explorer

Theorem bralnfn

Description: The Dirac bra function is a linear functional. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	bralnfn	$⊢ A \in ℋ \to bra (A) \in LinFn$

Proof

Step	Hyp	Ref	Expression
1		brafn	$⊢ A \in ℋ \to bra (A) : ℋ ⟶ ℂ$
2		simpll	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to A \in ℋ$
3		hvmulcl	$⊢ (x \in ℂ \land y \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
4	3	ad2ant2lr	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to x \cdot_{ℎ} y \in ℋ$
5		simprr	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to z \in ℋ$
6		braadd	$⊢ (A \in ℋ \land x \cdot_{ℎ} y \in ℋ \land z \in ℋ) \to bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = bra (A) (x \cdot_{ℎ} y) + bra (A) (z)$
7	2 4 5 6	syl3anc	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = bra (A) (x \cdot_{ℎ} y) + bra (A) (z)$
8		bramul	$⊢ (A \in ℋ \land x \in ℂ \land y \in ℋ) \to bra (A) (x \cdot_{ℎ} y) = x bra (A) (y)$
9	8	3expa	$⊢ ((A \in ℋ \land x \in ℂ) \land y \in ℋ) \to bra (A) (x \cdot_{ℎ} y) = x bra (A) (y)$
10	9	adantrr	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to bra (A) (x \cdot_{ℎ} y) = x bra (A) (y)$
11	10	oveq1d	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to bra (A) (x \cdot_{ℎ} y) + bra (A) (z) = x bra (A) (y) + bra (A) (z)$
12	7 11	eqtrd	$⊢ ((A \in ℋ \land x \in ℂ) \land (y \in ℋ \land z \in ℋ)) \to bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = x bra (A) (y) + bra (A) (z)$
13	12	ralrimivva	$⊢ (A \in ℋ \land x \in ℂ) \to \forall y \in ℋ \forall z \in ℋ bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = x bra (A) (y) + bra (A) (z)$
14	13	ralrimiva	$⊢ A \in ℋ \to \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = x bra (A) (y) + bra (A) (z)$
15		ellnfn	$⊢ bra (A) \in LinFn \leftrightarrow (bra (A) : ℋ ⟶ ℂ \land \forall x \in ℂ \forall y \in ℋ \forall z \in ℋ bra (A) ((x \cdot_{ℎ} y) +_{ℎ} z) = x bra (A) (y) + bra (A) (z))$
16	1 14 15	sylanbrc	$⊢ A \in ℋ \to bra (A) \in LinFn$