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 : ~H --> ~H
	hoeq.2	|- T : ~H --> ~H
Assertion	hoaddcomi	|- ( S +op T ) = ( T +op S )

Proof

Step	Hyp	Ref	Expression
1		hoeq.1	|- S : ~H --> ~H
2		hoeq.2	|- T : ~H --> ~H
3	1	ffvelcdmi	|- ( x e. ~H -> ( S ` x ) e. ~H )
4	2	ffvelcdmi	|- ( x e. ~H -> ( T ` x ) e. ~H )
5		ax-hvcom	|- ( ( ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( S ` x ) +h ( T ` x ) ) = ( ( T ` x ) +h ( S ` x ) ) )
6	3 4 5	syl2anc	|- ( x e. ~H -> ( ( S ` x ) +h ( T ` x ) ) = ( ( T ` x ) +h ( S ` x ) ) )
7		hosval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )
8	1 2 7	mp3an12	|- ( x e. ~H -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )
9		hosval	|- ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ x e. ~H ) -> ( ( T +op S ) ` x ) = ( ( T ` x ) +h ( S ` x ) ) )
10	2 1 9	mp3an12	|- ( x e. ~H -> ( ( T +op S ) ` x ) = ( ( T ` x ) +h ( S ` x ) ) )
11	6 8 10	3eqtr4d	|- ( x e. ~H -> ( ( S +op T ) ` x ) = ( ( T +op S ) ` x ) )
12	11	rgen	|- A. x e. ~H ( ( S +op T ) ` x ) = ( ( T +op S ) ` x )
13	1 2	hoaddcli	|- ( S +op T ) : ~H --> ~H
14	2 1	hoaddcli	|- ( T +op S ) : ~H --> ~H
15	13 14	hoeqi	|- ( A. x e. ~H ( ( S +op T ) ` x ) = ( ( T +op S ) ` x ) <-> ( S +op T ) = ( T +op S ) )
16	12 15	mpbi	|- ( S +op T ) = ( T +op S )