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

Metamath Proof Explorer

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 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑆 ‘ 𝑥 ) ∈ ℋ )
4 2 ffvelcdmi ⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
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 𝑆 )