hosub4

Description: Rearrangement of 4 terms in a mixed addition and subtraction of Hilbert space operators. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hosub4	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) -_{op} (T +_{op} U) = (R -_{op} T) +_{op} (S -_{op} U)$

Proof

Step	Hyp	Ref	Expression
1		honegdi	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to -1 \cdot_{op} (T +_{op} U) = (-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} U)$
2	1	adantl	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to -1 \cdot_{op} (T +_{op} U) = (-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} U)$
3	2	oveq2d	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} (-1 \cdot_{op} (T +_{op} U)) = (R +_{op} S) +_{op} ((-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} U))$
4		neg1cn	$⊢ - 1 \in ℂ$
5		homulcl	$⊢ (- 1 \in ℂ \land T : ℋ ⟶ ℋ) \to (-1 \cdot_{op} T) : ℋ ⟶ ℋ$
6	4 5	mpan	$⊢ T : ℋ ⟶ ℋ \to (-1 \cdot_{op} T) : ℋ ⟶ ℋ$
7		homulcl	$⊢ (- 1 \in ℂ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
8	4 7	mpan	$⊢ U : ℋ ⟶ ℋ \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
9	6 8	anim12i	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((-1 \cdot_{op} T) : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ)$
10		hoadd4	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land ((-1 \cdot_{op} T) : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} ((-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} U)) = (R +_{op} (-1 \cdot_{op} T)) +_{op} (S +_{op} (-1 \cdot_{op} U))$
11	9 10	sylan2	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} ((-1 \cdot_{op} T) +_{op} (-1 \cdot_{op} U)) = (R +_{op} (-1 \cdot_{op} T)) +_{op} (S +_{op} (-1 \cdot_{op} U))$
12	3 11	eqtrd	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} (-1 \cdot_{op} (T +_{op} U)) = (R +_{op} (-1 \cdot_{op} T)) +_{op} (S +_{op} (-1 \cdot_{op} U))$
13		hoaddcl	$⊢ (R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \to (R +_{op} S) : ℋ ⟶ ℋ$
14		hoaddcl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T +_{op} U) : ℋ ⟶ ℋ$
15		honegsub	$⊢ ((R +_{op} S) : ℋ ⟶ ℋ \land (T +_{op} U) : ℋ ⟶ ℋ) \to (R +_{op} S) +_{op} (-1 \cdot_{op} (T +_{op} U)) = (R +_{op} S) -_{op} (T +_{op} U)$
16	13 14 15	syl2an	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) +_{op} (-1 \cdot_{op} (T +_{op} U)) = (R +_{op} S) -_{op} (T +_{op} U)$
17		honegsub	$⊢ (R : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to R +_{op} (-1 \cdot_{op} T) = R -_{op} T$
18	17	ad2ant2r	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to R +_{op} (-1 \cdot_{op} T) = R -_{op} T$
19		honegsub	$⊢ (S : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to S +_{op} (-1 \cdot_{op} U) = S -_{op} U$
20	19	ad2ant2l	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to S +_{op} (-1 \cdot_{op} U) = S -_{op} U$
21	18 20	oveq12d	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} (-1 \cdot_{op} T)) +_{op} (S +_{op} (-1 \cdot_{op} U)) = (R -_{op} T) +_{op} (S -_{op} U)$
22	12 16 21	3eqtr3d	$⊢ ((R : ℋ ⟶ ℋ \land S : ℋ ⟶ ℋ) \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (R +_{op} S) -_{op} (T +_{op} U) = (R -_{op} T) +_{op} (S -_{op} U)$

Metamath Proof Explorer

Theorem hosub4

Proof