hosd1i

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

Step	Hyp	Ref	Expression
1		hosd1.2	$⊢ T : ℋ ⟶ ℋ$
2		hosd1.3	$⊢ U : ℋ ⟶ ℋ$
3		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
4	3 2	hosubcli	$⊢ (0_{hop} -_{op} U) : ℋ ⟶ ℋ$
5	1 2	hoaddcli	$⊢ (T +_{op} U) : ℋ ⟶ ℋ$
6	4 5	hoaddcomi	$⊢ (0_{hop} -_{op} U) +_{op} (T +_{op} U) = (T +_{op} U) +_{op} (0_{hop} -_{op} U)$
7	5 3 2	hoaddsubassi	$⊢ ((T +_{op} U) +_{op} 0_{hop}) -_{op} U = (T +_{op} U) +_{op} (0_{hop} -_{op} U)$
8	6 7	eqtr4i	$⊢ (0_{hop} -_{op} U) +_{op} (T +_{op} U) = ((T +_{op} U) +_{op} 0_{hop}) -_{op} U$
9	5	hoaddridi	$⊢ (T +_{op} U) +_{op} 0_{hop} = T +_{op} U$
10	9	oveq1i	$⊢ ((T +_{op} U) +_{op} 0_{hop}) -_{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) : ℋ ⟶ ℋ$
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	$⊢ (0_{hop} -_{op} U) +_{op} (T +_{op} U) = T$
17	1 4 5	hodsi	$⊢ T -_{op} (0_{hop} -_{op} U) = T +_{op} U \leftrightarrow (0_{hop} -_{op} U) +_{op} (T +_{op} U) = T$
18	16 17	mpbir	$⊢ T -_{op} (0_{hop} -_{op} U) = T +_{op} U$
19	18	eqcomi	$⊢ T +_{op} U = T -_{op} (0_{hop} -_{op} U)$

Metamath Proof Explorer