ho2times

Description: Two times a Hilbert space operator. (Contributed by NM, 26-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	ho2times	$⊢ T : ℋ ⟶ ℋ \to 2 \cdot_{op} T = T +_{op} T$

Step	Hyp	Ref	Expression
1		df-2	$⊢ 2 = 1 + 1$
2	1	oveq1i	$⊢ 2 \cdot_{op} T = (1 + 1) \cdot_{op} T$
3		ax-1cn	$⊢ 1 \in ℂ$
4		hoadddir	$⊢ (1 \in ℂ \land 1 \in ℂ \land T : ℋ ⟶ ℋ) \to (1 + 1) \cdot_{op} T = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
5	3 3 4	mp3an12	$⊢ T : ℋ ⟶ ℋ \to (1 + 1) \cdot_{op} T = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
6	2 5	eqtrid	$⊢ T : ℋ ⟶ ℋ \to 2 \cdot_{op} T = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
7		hoadddi	$⊢ (1 \in ℂ \land T : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to 1 \cdot_{op} (T +_{op} T) = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
8	3 7	mp3an1	$⊢ (T : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to 1 \cdot_{op} (T +_{op} T) = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
9	8	anidms	$⊢ T : ℋ ⟶ ℋ \to 1 \cdot_{op} (T +_{op} T) = (1 \cdot_{op} T) +_{op} (1 \cdot_{op} T)$
10		hoaddcl	$⊢ (T : ℋ ⟶ ℋ \land T : ℋ ⟶ ℋ) \to (T +_{op} T) : ℋ ⟶ ℋ$
11	10	anidms	$⊢ T : ℋ ⟶ ℋ \to (T +_{op} T) : ℋ ⟶ ℋ$
12		homulid2	$⊢ (T +_{op} T) : ℋ ⟶ ℋ \to 1 \cdot_{op} (T +_{op} T) = T +_{op} T$
13	11 12	syl	$⊢ T : ℋ ⟶ ℋ \to 1 \cdot_{op} (T +_{op} T) = T +_{op} T$
14	6 9 13	3eqtr2d	$⊢ T : ℋ ⟶ ℋ \to 2 \cdot_{op} T = T +_{op} T$

Metamath Proof Explorer