Metamath Proof Explorer

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

Proof

Step	Hyp	Ref	Expression
1		hoadd32	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) = ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) )
2	1	oveq1d	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) )
3	2	3expa	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) )
4	3	adantrr	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) )
5		hoaddcl	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) → ( 𝑅 +_op 𝑆 ) : ℋ ⟶ ℋ )
6		hoaddass	⊢ ( ( ( 𝑅 +_op 𝑆 ) : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑆 ) +_op ( 𝑇 +_op 𝑈 ) ) )
7	6	3expb	⊢ ( ( ( 𝑅 +_op 𝑆 ) : ℋ ⟶ ℋ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑆 ) +_op ( 𝑇 +_op 𝑈 ) ) )
8	5 7	sylan	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑆 ) +_op 𝑇 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑆 ) +_op ( 𝑇 +_op 𝑈 ) ) )
9		hoaddcl	⊢ ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑅 +_op 𝑇 ) : ℋ ⟶ ℋ )
10		hoaddass	⊢ ( ( ( 𝑅 +_op 𝑇 ) : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) → ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑇 ) +_op ( 𝑆 +_op 𝑈 ) ) )
11	10	3expb	⊢ ( ( ( 𝑅 +_op 𝑇 ) : ℋ ⟶ ℋ ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑇 ) +_op ( 𝑆 +_op 𝑈 ) ) )
12	9 11	sylan	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑇 ) +_op ( 𝑆 +_op 𝑈 ) ) )
13	12	an4s	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( ( 𝑅 +_op 𝑇 ) +_op 𝑆 ) +_op 𝑈 ) = ( ( 𝑅 +_op 𝑇 ) +_op ( 𝑆 +_op 𝑈 ) ) )
14	4 8 13	3eqtr3d	⊢ ( ( ( 𝑅 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ) ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ) → ( ( 𝑅 +_op 𝑆 ) +_op ( 𝑇 +_op 𝑈 ) ) = ( ( 𝑅 +_op 𝑇 ) +_op ( 𝑆 +_op 𝑈 ) ) )