Theorem hosd2i

Description: Hilbert space operator sum expressed in terms of difference. (Contributed by NM, 27-Aug-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hosd1.2	|- T : ~H --> ~H
	hosd1.3	|- U : ~H --> ~H
Assertion	hosd2i	|- ( T +op U ) = ( T -op ( ( U -op U ) -op U ) )

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	|- T : ~H --> ~H
2		hosd1.3	|- U : ~H --> ~H
3	1 2	hosd1i	|- ( T +op U ) = ( T -op ( 0hop -op U ) )
4	2	hodidi	|- ( U -op U ) = 0hop
5	4	oveq1i	|- ( ( U -op U ) -op U ) = ( 0hop -op U )
6	5	oveq2i	|- ( T -op ( ( U -op U ) -op U ) ) = ( T -op ( 0hop -op U ) )
7	3 6	eqtr4i	|- ( T +op U ) = ( T -op ( ( U -op U ) -op U ) )