Theorem hosubadd4

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

	Ref	Expression
Assertion	hosubadd4	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 −op 𝑆 ) −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑅 +op 𝑈 ) −op ( 𝑆 +op 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hosubcl	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( 𝑅 −op 𝑆 ) : ℋ ⟶ ℋ )
2		hosubsub2	⊢ ( ( ( 𝑅 −op 𝑆 ) : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( 𝑅 −op 𝑆 ) −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑈 −op 𝑇 ) ) )
3	2	3expb	⊢ ( ( ( 𝑅 −op 𝑆 ) : ℋ ⟶ ℋ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 −op 𝑆 ) −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑈 −op 𝑇 ) ) )
4	1 3	sylan	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 −op 𝑆 ) −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑈 −op 𝑇 ) ) )
5		hosub4	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑈 ) −op ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑈 −op 𝑇 ) ) )
6	5	an42s	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +op 𝑈 ) −op ( 𝑆 +op 𝑇 ) ) = ( ( 𝑅 −op 𝑆 ) +op ( 𝑈 −op 𝑇 ) ) )
7	4 6	eqtr4d	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 −op 𝑆 ) −op ( 𝑇 −op 𝑈 ) ) = ( ( 𝑅 +op 𝑈 ) −op ( 𝑆 +op 𝑇 ) ) )