hoadddir

Description: Scalar product reverse distributive law for Hilbert space operators. (Contributed by NM, 25-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	hoadddir	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to (A + B) \cdot_{op} T = (A \cdot_{op} T) +_{op} (B \cdot_{op} T)$

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
2	1	anim1i	$⊢ ((A \in ℂ \land B \in ℂ) \land T : ℋ ⟶ ℋ) \to (A + B \in ℂ \land T : ℋ ⟶ ℋ)$
3	2	3impa	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to (A + B \in ℂ \land T : ℋ ⟶ ℋ)$
4		homval	$⊢ (A + B \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to ((A + B) \cdot_{op} T) (x) = (A + B) \cdot_{ℎ} T (x)$
5	4	3expa	$⊢ ((A + B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A + B) \cdot_{op} T) (x) = (A + B) \cdot_{ℎ} T (x)$
6	3 5	sylan	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A + B) \cdot_{op} T) (x) = (A + B) \cdot_{ℎ} T (x)$
7		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
8	7	3expa	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
9	8	3adantl2	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
10		homval	$⊢ (B \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (B \cdot_{op} T) (x) = B \cdot_{ℎ} T (x)$
11	10	3expa	$⊢ ((B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (B \cdot_{op} T) (x) = B \cdot_{ℎ} T (x)$
12	11	3adantl1	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (B \cdot_{op} T) (x) = B \cdot_{ℎ} T (x)$
13	9 12	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x))$
14		ffvelcdm	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to T (x) \in ℋ$
15		ax-hvdistr2	$⊢ (A \in ℂ \land B \in ℂ \land T (x) \in ℋ) \to (A + B) \cdot_{ℎ} T (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x))$
16	14 15	syl3an3	$⊢ (A \in ℂ \land B \in ℂ \land (T : ℋ ⟶ ℋ \land x \in ℋ)) \to (A + B) \cdot_{ℎ} T (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x))$
17	16	3exp	$⊢ A \in ℂ \to (B \in ℂ \to ((T : ℋ ⟶ ℋ \land x \in ℋ) \to (A + B) \cdot_{ℎ} T (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x))))$
18	17	exp4a	$⊢ A \in ℂ \to (B \in ℂ \to (T : ℋ ⟶ ℋ \to (x \in ℋ \to (A + B) \cdot_{ℎ} T (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x)))))$
19	18	3imp1	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A + B) \cdot_{ℎ} T (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (B \cdot_{ℎ} T (x))$
20	13 19	eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x) = (A + B) \cdot_{ℎ} T (x)$
21	6 20	eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A + B) \cdot_{op} T) (x) = (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x)$
22		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
23		homulcl	$⊢ (B \in ℂ \land T : ℋ ⟶ ℋ) \to (B \cdot_{op} T) : ℋ ⟶ ℋ$
24	22 23	anim12i	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (B \in ℂ \land T : ℋ ⟶ ℋ)) \to ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (B \cdot_{op} T) : ℋ ⟶ ℋ)$
25	24	3impdir	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (B \cdot_{op} T) : ℋ ⟶ ℋ)$
26		hosval	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (B \cdot_{op} T) : ℋ ⟶ ℋ \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x)$
27	26	3expa	$⊢ (((A \cdot_{op} T) : ℋ ⟶ ℋ \land (B \cdot_{op} T) : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x)$
28	25 27	sylan	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (B \cdot_{op} T) (x)$
29	21 28	eqtr4d	$⊢ ((A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A + B) \cdot_{op} T) (x) = ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x)$
30	29	ralrimiva	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to \forall x \in ℋ ((A + B) \cdot_{op} T) (x) = ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x)$
31		homulcl	$⊢ (A + B \in ℂ \land T : ℋ ⟶ ℋ) \to ((A + B) \cdot_{op} T) : ℋ ⟶ ℋ$
32	1 31	stoic3	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to ((A + B) \cdot_{op} T) : ℋ ⟶ ℋ$
33		hoaddcl	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (B \cdot_{op} T) : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) : ℋ ⟶ ℋ$
34	22 23 33	syl2an	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (B \in ℂ \land T : ℋ ⟶ ℋ)) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) : ℋ ⟶ ℋ$
35	34	3impdir	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) : ℋ ⟶ ℋ$
36		hoeq	$⊢ (((A + B) \cdot_{op} T) : ℋ ⟶ ℋ \land ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) : ℋ ⟶ ℋ) \to (\forall x \in ℋ ((A + B) \cdot_{op} T) (x) = ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x) \leftrightarrow (A + B) \cdot_{op} T = (A \cdot_{op} T) +_{op} (B \cdot_{op} T))$
37	32 35 36	syl2anc	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to (\forall x \in ℋ ((A + B) \cdot_{op} T) (x) = ((A \cdot_{op} T) +_{op} (B \cdot_{op} T)) (x) \leftrightarrow (A + B) \cdot_{op} T = (A \cdot_{op} T) +_{op} (B \cdot_{op} T))$
38	30 37	mpbid	$⊢ (A \in ℂ \land B \in ℂ \land T : ℋ ⟶ ℋ) \to (A + B) \cdot_{op} T = (A \cdot_{op} T) +_{op} (B \cdot_{op} T)$

Metamath Proof Explorer

Theorem hoadddir

Proof