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 ⊢ S : ℋ ⟶ ℋ
hoeq.2 ⊢ T : ℋ ⟶ ℋ
Assertion hoaddcomi ⊢ S + op T = T + op S

Proof

Step Hyp Ref Expression
1 hoeq.1 ⊢ S : ℋ ⟶ ℋ
2 hoeq.2 ⊢ T : ℋ ⟶ ℋ
3 1 ffvelcdmi ⊢ x ∈ ℋ → S ⁡ x ∈ ℋ
4 2 ffvelcdmi ⊢ x ∈ ℋ → T ⁡ x ∈ ℋ
5 ax-hvcom ⊢ S ⁡ x ∈ ℋ ∧ T ⁡ x ∈ ℋ → S ⁡ x + ℎ T ⁡ x = T ⁡ x + ℎ S ⁡ x
6 3 4 5 syl2anc ⊢ x ∈ ℋ → S ⁡ x + ℎ T ⁡ x = T ⁡ x + ℎ S ⁡ x
7 hosval ⊢ S : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → S + op T ⁡ x = S ⁡ x + ℎ T ⁡ x
8 1 2 7 mp3an12 ⊢ x ∈ ℋ → S + op T ⁡ x = S ⁡ x + ℎ T ⁡ x
9 hosval ⊢ T : ℋ ⟶ ℋ ∧ S : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op S ⁡ x = T ⁡ x + ℎ S ⁡ x
10 2 1 9 mp3an12 ⊢ x ∈ ℋ → T + op S ⁡ x = T ⁡ x + ℎ S ⁡ x
11 6 8 10 3eqtr4d ⊢ x ∈ ℋ → S + op T ⁡ x = T + op S ⁡ x
12 11 rgen ⊢ ∀ x ∈ ℋ S + op T ⁡ x = T + op S ⁡ x
13 1 2 hoaddcli ⊢ S + op T : ℋ ⟶ ℋ
14 2 1 hoaddcli ⊢ T + op S : ℋ ⟶ ℋ
15 13 14 hoeqi ⊢ ∀ x ∈ ℋ S + op T ⁡ x = T + op S ⁡ x ↔ S + op T = T + op S
16 12 15 mpbi ⊢ S + op T = T + op S