Theorem hoaddcom

Description: Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoaddcom	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( 𝑆 +op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op 𝑇 ) )
2		oveq2	⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( 𝑇 +op 𝑆 ) = ( 𝑇 +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) )
3	1 2	eqeq12d	⊢ ( 𝑆 = if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) → ( ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) ↔ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op 𝑇 ) = ( 𝑇 +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) ) )
4		oveq2	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op 𝑇 ) = ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) )
5		oveq1	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( 𝑇 +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) )
6	4 5	eqeq12d	⊢ ( 𝑇 = if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) → ( ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op 𝑇 ) = ( 𝑇 +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) ↔ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) ) ) )
7		ho0f	⊢ 0hop : ℋ ⟶ ℋ
8	7	elimf	⊢ if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) : ℋ ⟶ ℋ
9	7	elimf	⊢ if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) : ℋ ⟶ ℋ
10	8 9	hoaddcomi	⊢ ( if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) +op if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) ) = ( if ( 𝑇 : ℋ ⟶ ℋ , 𝑇 , 0hop ) +op if ( 𝑆 : ℋ ⟶ ℋ , 𝑆 , 0hop ) )
11	3 6 10	dedth2h	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )