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 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