Theorem hosd1i

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	hosd1i	|- ( T +op U ) = ( T -op ( 0hop -op U ) )

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	|- T : ~H --> ~H
2		hosd1.3	|- U : ~H --> ~H
3		ho0f	|- 0hop : ~H --> ~H
4	3 2	hosubcli	|- ( 0hop -op U ) : ~H --> ~H
5	1 2	hoaddcli	|- ( T +op U ) : ~H --> ~H
6	4 5	hoaddcomi	|- ( ( 0hop -op U ) +op ( T +op U ) ) = ( ( T +op U ) +op ( 0hop -op U ) )
7	5 3 2	hoaddsubassi	|- ( ( ( T +op U ) +op 0hop ) -op U ) = ( ( T +op U ) +op ( 0hop -op U ) )
8	6 7	eqtr4i	|- ( ( 0hop -op U ) +op ( T +op U ) ) = ( ( ( T +op U ) +op 0hop ) -op U )
9	5	hoaddid1i	|- ( ( T +op U ) +op 0hop ) = ( T +op U )
10	9	oveq1i	|- ( ( ( T +op U ) +op 0hop ) -op U ) = ( ( T +op U ) -op U )
11	1 2 2	hoaddsubi	|- ( ( T +op U ) -op U ) = ( ( T -op U ) +op U )
12	1 2	hosubcli	|- ( T -op U ) : ~H --> ~H
13	12 2	hoaddcomi	|- ( ( T -op U ) +op U ) = ( U +op ( T -op U ) )
14	2 1	hodseqi	|- ( U +op ( T -op U ) ) = T
15	11 13 14	3eqtri	|- ( ( T +op U ) -op U ) = T
16	8 10 15	3eqtri	|- ( ( 0hop -op U ) +op ( T +op U ) ) = T
17	1 4 5	hodsi	|- ( ( T -op ( 0hop -op U ) ) = ( T +op U ) <-> ( ( 0hop -op U ) +op ( T +op U ) ) = T )
18	16 17	mpbir	|- ( T -op ( 0hop -op U ) ) = ( T +op U )
19	18	eqcomi	|- ( T +op U ) = ( T -op ( 0hop -op U ) )