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

Metamath Proof Explorer

Theorem honegsub

Description: Relationship between Hilbert space operator addition and subtraction. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion honegsub ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → T + op -1 · op U = T - op U

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ T = if T : ℋ ⟶ ℋ T 0 hop → T + op -1 · op U = if T : ℋ ⟶ ℋ T 0 hop + op -1 · op U
2 oveq1 ⊢ T = if T : ℋ ⟶ ℋ T 0 hop → T - op U = if T : ℋ ⟶ ℋ T 0 hop - op U
3 1 2 eqeq12d ⊢ T = if T : ℋ ⟶ ℋ T 0 hop → T + op -1 · op U = T - op U ↔ if T : ℋ ⟶ ℋ T 0 hop + op -1 · op U = if T : ℋ ⟶ ℋ T 0 hop - op U
4 oveq2 ⊢ U = if U : ℋ ⟶ ℋ U 0 hop → -1 · op U = -1 · op if U : ℋ ⟶ ℋ U 0 hop
5 4 oveq2d ⊢ U = if U : ℋ ⟶ ℋ U 0 hop → if T : ℋ ⟶ ℋ T 0 hop + op -1 · op U = if T : ℋ ⟶ ℋ T 0 hop + op -1 · op if U : ℋ ⟶ ℋ U 0 hop
6 oveq2 ⊢ U = if U : ℋ ⟶ ℋ U 0 hop → if T : ℋ ⟶ ℋ T 0 hop - op U = if T : ℋ ⟶ ℋ T 0 hop - op if U : ℋ ⟶ ℋ U 0 hop
7 5 6 eqeq12d ⊢ U = if U : ℋ ⟶ ℋ U 0 hop → if T : ℋ ⟶ ℋ T 0 hop + op -1 · op U = if T : ℋ ⟶ ℋ T 0 hop - op U ↔ if T : ℋ ⟶ ℋ T 0 hop + op -1 · op if U : ℋ ⟶ ℋ U 0 hop = if T : ℋ ⟶ ℋ T 0 hop - op if U : ℋ ⟶ ℋ U 0 hop
8 ho0f ⊢ 0 hop : ℋ ⟶ ℋ
9 8 elimf ⊢ if T : ℋ ⟶ ℋ T 0 hop : ℋ ⟶ ℋ
10 8 elimf ⊢ if U : ℋ ⟶ ℋ U 0 hop : ℋ ⟶ ℋ
11 9 10 honegsubi ⊢ if T : ℋ ⟶ ℋ T 0 hop + op -1 · op if U : ℋ ⟶ ℋ U 0 hop = if T : ℋ ⟶ ℋ T 0 hop - op if U : ℋ ⟶ ℋ U 0 hop
12 3 7 11 dedth2h ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ → T + op -1 · op U = T - op U