Theorem hoadd4

Description: Rearrangement of 4 terms in a sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoadd4	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hoadd32	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S$$
2	1	oveq1d	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U$$
3	2	3expa	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U$$
4	3	adantrr	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U$$
5		hoaddcl	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}$$
6		hoaddass	$$⊢\left(\left(R{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$
7	6	3expb	$$⊢\left(\left(R{+}_{\mathrm{op}}S\right):\mathscr{H}⟶\mathscr{H}\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$
8	5 7	sylan	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)$$
9		hoaddcl	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}$$
10		hoaddass	$$⊢\left(\left(R{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\to \left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$
11	10	3expb	$$⊢\left(\left(R{+}_{\mathrm{op}}T\right):\mathscr{H}⟶\mathscr{H}\wedge \left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$
12	9 11	sylan	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(S:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$
13	12	an4s	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}U=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$
14	4 8 13	3eqtr3d	$$⊢\left(\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\wedge \left(T:\mathscr{H}⟶\mathscr{H}\wedge U:\mathscr{H}⟶\mathscr{H}\right)\right)\to \left(R{+}_{\mathrm{op}}S\right){+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}U\right)=\left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}U\right)$$