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

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