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	⊢ 𝑇 : ℋ ⟶ ℋ
	hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
Assertion	hosd1i	⊢ ( 𝑇 +op 𝑈 ) = ( 𝑇 −op ( 0hop −op 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		hosd1.2	⊢ 𝑇 : ℋ ⟶ ℋ
2		hosd1.3	⊢ 𝑈 : ℋ ⟶ ℋ
3		ho0f	⊢ 0hop : ℋ ⟶ ℋ
4	3 2	hosubcli	⊢ ( 0hop −op 𝑈 ) : ℋ ⟶ ℋ
5	1 2	hoaddcli	⊢ ( 𝑇 +op 𝑈 ) : ℋ ⟶ ℋ
6	4 5	hoaddcomi	⊢ ( ( 0hop −op 𝑈 ) +op ( 𝑇 +op 𝑈 ) ) = ( ( 𝑇 +op 𝑈 ) +op ( 0hop −op 𝑈 ) )
7	5 3 2	hoaddsubassi	⊢ ( ( ( 𝑇 +op 𝑈 ) +op 0hop ) −op 𝑈 ) = ( ( 𝑇 +op 𝑈 ) +op ( 0hop −op 𝑈 ) )
8	6 7	eqtr4i	⊢ ( ( 0hop −op 𝑈 ) +op ( 𝑇 +op 𝑈 ) ) = ( ( ( 𝑇 +op 𝑈 ) +op 0hop ) −op 𝑈 )
9	5	hoaddridi	⊢ ( ( 𝑇 +op 𝑈 ) +op 0hop ) = ( 𝑇 +op 𝑈 )
10	9	oveq1i	⊢ ( ( ( 𝑇 +op 𝑈 ) +op 0hop ) −op 𝑈 ) = ( ( 𝑇 +op 𝑈 ) −op 𝑈 )
11	1 2 2	hoaddsubi	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = ( ( 𝑇 −op 𝑈 ) +op 𝑈 )
12	1 2	hosubcli	⊢ ( 𝑇 −op 𝑈 ) : ℋ ⟶ ℋ
13	12 2	hoaddcomi	⊢ ( ( 𝑇 −op 𝑈 ) +op 𝑈 ) = ( 𝑈 +op ( 𝑇 −op 𝑈 ) )
14	2 1	hodseqi	⊢ ( 𝑈 +op ( 𝑇 −op 𝑈 ) ) = 𝑇
15	11 13 14	3eqtri	⊢ ( ( 𝑇 +op 𝑈 ) −op 𝑈 ) = 𝑇
16	8 10 15	3eqtri	⊢ ( ( 0hop −op 𝑈 ) +op ( 𝑇 +op 𝑈 ) ) = 𝑇
17	1 4 5	hodsi	⊢ ( ( 𝑇 −op ( 0hop −op 𝑈 ) ) = ( 𝑇 +op 𝑈 ) ↔ ( ( 0hop −op 𝑈 ) +op ( 𝑇 +op 𝑈 ) ) = 𝑇 )
18	16 17	mpbir	⊢ ( 𝑇 −op ( 0hop −op 𝑈 ) ) = ( 𝑇 +op 𝑈 )
19	18	eqcomi	⊢ ( 𝑇 +op 𝑈 ) = ( 𝑇 −op ( 0hop −op 𝑈 ) )