This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) ) )