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

Metamath Proof Explorer

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