Theorem hfsval

Description: Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hfsval	$$⊢\left(S:\mathscr{H}⟶ℂ\wedge T:\mathscr{H}⟶ℂ\wedge A\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{fn}}T\right)\left(A\right)=S\left(A\right)+T\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		hfsmval	$$⊢\left(S:\mathscr{H}⟶ℂ\wedge T:\mathscr{H}⟶ℂ\right)\to S{+}_{\mathrm{fn}}T=\left(x\in \mathscr{H}⟼S\left(x\right)+T\left(x\right)\right)$$
2	1	fveq1d	$$⊢\left(S:\mathscr{H}⟶ℂ\wedge T:\mathscr{H}⟶ℂ\right)\to \left(S{+}_{\mathrm{fn}}T\right)\left(A\right)=\left(x\in \mathscr{H}⟼S\left(x\right)+T\left(x\right)\right)\left(A\right)$$
3		fveq2	$$⊢x=A\to S\left(x\right)=S\left(A\right)$$
4		fveq2	$$⊢x=A\to T\left(x\right)=T\left(A\right)$$
5	3 4	oveq12d	$$⊢x=A\to S\left(x\right)+T\left(x\right)=S\left(A\right)+T\left(A\right)$$
6		eqid	$$⊢\left(x\in \mathscr{H}⟼S\left(x\right)+T\left(x\right)\right)=\left(x\in \mathscr{H}⟼S\left(x\right)+T\left(x\right)\right)$$
7		ovex	$$⊢S\left(A\right)+T\left(A\right)\in \mathrm{V}$$
8	5 6 7	fvmpt	$$⊢A\in \mathscr{H}\to \left(x\in \mathscr{H}⟼S\left(x\right)+T\left(x\right)\right)\left(A\right)=S\left(A\right)+T\left(A\right)$$
9	2 8	sylan9eq	$$⊢\left(\left(S:\mathscr{H}⟶ℂ\wedge T:\mathscr{H}⟶ℂ\right)\wedge A\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{fn}}T\right)\left(A\right)=S\left(A\right)+T\left(A\right)$$
10	9	3impa	$$⊢\left(S:\mathscr{H}⟶ℂ\wedge T:\mathscr{H}⟶ℂ\wedge A\in \mathscr{H}\right)\to \left(S{+}_{\mathrm{fn}}T\right)\left(A\right)=S\left(A\right)+T\left(A\right)$$