This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑈 ) )