Theorem lnopaddi

Description: Additive property of a linear Hilbert space operator. (Contributed by NM, 11-May-2005) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnopl.1	$$⊢T\in \mathrm{LinOp}$$
Assertion	lnopaddi	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}B\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		lnopl.1	$$⊢T\in \mathrm{LinOp}$$
2		ax-1cn	$$⊢1\in ℂ$$
3	1	lnopli	$$⊢\left(1\in ℂ\wedge A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}B\right)=\left(1{\cdot }_{ℎ}T\left(A\right)\right){+}_{ℎ}T\left(B\right)$$
4	2 3	mp3an1	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}B\right)=\left(1{\cdot }_{ℎ}T\left(A\right)\right){+}_{ℎ}T\left(B\right)$$
5		ax-hvmulid	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}A=A$$
6	5	fvoveq1d	$$⊢A\in \mathscr{H}\to T\left(\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}B\right)=T\left(A{+}_{ℎ}B\right)$$
7	6	adantr	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}B\right)=T\left(A{+}_{ℎ}B\right)$$
8	1	lnopfi	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
9	8	ffvelcdmi	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
10		ax-hvmulid	$$⊢T\left(A\right)\in \mathscr{H}\to 1{\cdot }_{ℎ}T\left(A\right)=T\left(A\right)$$
11	9 10	syl	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}T\left(A\right)=T\left(A\right)$$
12	11	adantr	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to 1{\cdot }_{ℎ}T\left(A\right)=T\left(A\right)$$
13	12	oveq1d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(1{\cdot }_{ℎ}T\left(A\right)\right){+}_{ℎ}T\left(B\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$
14	4 7 13	3eqtr3d	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to T\left(A{+}_{ℎ}B\right)=T\left(A\right){+}_{ℎ}T\left(B\right)$$