# 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 \mathrm{bra}\left({A}\right)\in \mathrm{LinFn}$

### Proof

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