Theorem hoaddcomi

Description: Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hoeq.1	⊢ 𝑆 : ℋ ⟶ ℋ
	hoeq.2	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	hoaddcomi	⊢ ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	⊢ 𝑆 : ℋ ⟶ ℋ
2		hoeq.2	⊢ 𝑇 : ℋ ⟶ ℋ
3	1	ffvelrni	⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
4	2	ffvelrni	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
5		ax-hvcom	⊢ ( ( ( 𝑆 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
6	3 4 5	syl2anc	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
7		hosval	⊢ ( ( 𝑆 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
8	1 2 7	mp3an12	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑆 ‘ 𝑥 ) +ℎ ( 𝑇 ‘ 𝑥 ) ) )
9		hosval	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑆 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 +op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
10	2 1 9	mp3an12	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 +op 𝑆 ) ‘ 𝑥 ) = ( ( 𝑇 ‘ 𝑥 ) +ℎ ( 𝑆 ‘ 𝑥 ) ) )
11	6 8 10	3eqtr4d	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 +op 𝑆 ) ‘ 𝑥 ) )
12	11	rgen	⊢ ∀ 𝑥 ∈ ℋ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 +op 𝑆 ) ‘ 𝑥 )
13	1 2	hoaddcli	⊢ ( 𝑆 +op 𝑇 ) : ℋ ⟶ ℋ
14	2 1	hoaddcli	⊢ ( 𝑇 +op 𝑆 ) : ℋ ⟶ ℋ
15	13 14	hoeqi	⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 +op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑇 +op 𝑆 ) ‘ 𝑥 ) ↔ ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 ) )
16	12 15	mpbi	⊢ ( 𝑆 +op 𝑇 ) = ( 𝑇 +op 𝑆 )