# Metamath Proof Explorer

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 ffvelrni $⊢ x ∈ ℋ → S ⁡ x ∈ ℋ$
4 2 ffvelrni $⊢ 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$