Theorem hodsi

Description: Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hods.1	|- R : ~H --> ~H
	hods.2	|- S : ~H --> ~H
	hods.3	|- T : ~H --> ~H
Assertion	hodsi	|- ( ( R -op S ) = T <-> ( S +op T ) = R )

Proof

Step	Hyp	Ref	Expression
1		hods.1	|- R : ~H --> ~H
2		hods.2	|- S : ~H --> ~H
3		hods.3	|- T : ~H --> ~H
4	1	ffvelcdmi	|- ( x e. ~H -> ( R ` x ) e. ~H )
5	2	ffvelcdmi	|- ( x e. ~H -> ( S ` x ) e. ~H )
6	3	ffvelcdmi	|- ( x e. ~H -> ( T ` x ) e. ~H )
7		hvsubadd	|- ( ( ( R ` x ) e. ~H /\ ( S ` x ) e. ~H /\ ( T ` x ) e. ~H ) -> ( ( ( R ` x ) -h ( S ` x ) ) = ( T ` x ) <-> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) )
8	4 5 6 7	syl3anc	|- ( x e. ~H -> ( ( ( R ` x ) -h ( S ` x ) ) = ( T ` x ) <-> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) )
9		hodval	|- ( ( R : ~H --> ~H /\ S : ~H --> ~H /\ x e. ~H ) -> ( ( R -op S ) ` x ) = ( ( R ` x ) -h ( S ` x ) ) )
10	1 2 9	mp3an12	|- ( x e. ~H -> ( ( R -op S ) ` x ) = ( ( R ` x ) -h ( S ` x ) ) )
11	10	eqeq1d	|- ( x e. ~H -> ( ( ( R -op S ) ` x ) = ( T ` x ) <-> ( ( R ` x ) -h ( S ` x ) ) = ( T ` x ) ) )
12		hosval	|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )
13	2 3 12	mp3an12	|- ( x e. ~H -> ( ( S +op T ) ` x ) = ( ( S ` x ) +h ( T ` x ) ) )
14	13	eqeq1d	|- ( x e. ~H -> ( ( ( S +op T ) ` x ) = ( R ` x ) <-> ( ( S ` x ) +h ( T ` x ) ) = ( R ` x ) ) )
15	8 11 14	3bitr4d	|- ( x e. ~H -> ( ( ( R -op S ) ` x ) = ( T ` x ) <-> ( ( S +op T ) ` x ) = ( R ` x ) ) )
16	15	ralbiia	|- ( A. x e. ~H ( ( R -op S ) ` x ) = ( T ` x ) <-> A. x e. ~H ( ( S +op T ) ` x ) = ( R ` x ) )
17	1 2	hosubcli	|- ( R -op S ) : ~H --> ~H
18	17 3	hoeqi	|- ( A. x e. ~H ( ( R -op S ) ` x ) = ( T ` x ) <-> ( R -op S ) = T )
19	2 3	hoaddcli	|- ( S +op T ) : ~H --> ~H
20	19 1	hoeqi	|- ( A. x e. ~H ( ( S +op T ) ` x ) = ( R ` x ) <-> ( S +op T ) = R )
21	16 18 20	3bitr3i	|- ( ( R -op S ) = T <-> ( S +op T ) = R )