Theorem hoadd32

Description: Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	$$⊢\left(S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$
2	1	3adant1	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to S{+}_{\mathrm{op}}T=T{+}_{\mathrm{op}}S$$
3	2	oveq2d	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)=R{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}S\right)$$
4		hoaddass	$$⊢\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=R{+}_{\mathrm{op}}\left(S{+}_{\mathrm{op}}T\right)$$
5		hoaddass	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S=R{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}S\right)$$
6	5	3com23	$$⊢\left(R:\mathscr{H}⟶\mathscr{H}\wedge S:\mathscr{H}⟶\mathscr{H}\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(R{+}_{\mathrm{op}}T\right){+}_{\mathrm{op}}S=R{+}_{\mathrm{op}}\left(T{+}_{\mathrm{op}}S\right)$$
7	3 4 6	3eqtr4d	$$⊢\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$$