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	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		hoaddcom	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )
2	1	3adant1	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )
3	2	oveq2d	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) = ( 𝑅 +op ( 𝑇 +op 𝑆 ) ) )
4		hoaddass	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( 𝑅 +op ( 𝑆 +op 𝑇 ) ) )
5		hoaddass	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) = ( 𝑅 +op ( 𝑇 +op 𝑆 ) ) )
6	5	3com23	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) = ( 𝑅 +op ( 𝑇 +op 𝑆 ) ) )
7	3 4 6	3eqtr4d	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑅 +op 𝑆 ) +op 𝑇 ) = ( ( 𝑅 +op 𝑇 ) +op 𝑆 ) )