Metamath Proof Explorer

Theorem hosubdi

Description: Scalar product distributive law for operator difference. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hosubdi	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T -_{op} U) = (A \cdot_{op} T) -_{op} (A \cdot_{op} U)$

Proof

Step	Hyp	Ref	Expression
1		neg1cn	$⊢ - 1 \in ℂ$
2		homulcl	$⊢ (- 1 \in ℂ \land U : ℋ ⟶ ℋ) \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
3	1 2	mpan	$⊢ U : ℋ ⟶ ℋ \to (-1 \cdot_{op} U) : ℋ ⟶ ℋ$
4		hoadddi	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land (-1 \cdot_{op} U) : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = (A \cdot_{op} T) +_{op} (A \cdot_{op} (-1 \cdot_{op} U))$
5	3 4	syl3an3	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = (A \cdot_{op} T) +_{op} (A \cdot_{op} (-1 \cdot_{op} U))$
6		homul12	$⊢ (A \in ℂ \land - 1 \in ℂ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (-1 \cdot_{op} U) = -1 \cdot_{op} (A \cdot_{op} U)$
7	1 6	mp3an2	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (-1 \cdot_{op} U) = -1 \cdot_{op} (A \cdot_{op} U)$
8	7	3adant2	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (-1 \cdot_{op} U) = -1 \cdot_{op} (A \cdot_{op} U)$
9	8	oveq2d	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} T) +_{op} (A \cdot_{op} (-1 \cdot_{op} U)) = (A \cdot_{op} T) +_{op} (-1 \cdot_{op} (A \cdot_{op} U))$
10	5 9	eqtrd	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = (A \cdot_{op} T) +_{op} (-1 \cdot_{op} (A \cdot_{op} U))$
11		honegsub	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to T +_{op} (-1 \cdot_{op} U) = T -_{op} U$
12	11	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = A \cdot_{op} (T -_{op} U)$
13	12	3adant1	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} (-1 \cdot_{op} U)) = A \cdot_{op} (T -_{op} U)$
14		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
15		homulcl	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} U) : ℋ ⟶ ℋ$
16		honegsub	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ) \to (A \cdot_{op} T) +_{op} (-1 \cdot_{op} (A \cdot_{op} U)) = (A \cdot_{op} T) -_{op} (A \cdot_{op} U)$
17	14 15 16	syl2an	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (A \in ℂ \land U : ℋ ⟶ ℋ)) \to (A \cdot_{op} T) +_{op} (-1 \cdot_{op} (A \cdot_{op} U)) = (A \cdot_{op} T) -_{op} (A \cdot_{op} U)$
18	17	3impdi	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} T) +_{op} (-1 \cdot_{op} (A \cdot_{op} U)) = (A \cdot_{op} T) -_{op} (A \cdot_{op} U)$
19	10 13 18	3eqtr3d	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T -_{op} U) = (A \cdot_{op} T) -_{op} (A \cdot_{op} U)$