hoadddi

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

		Ref	Expression
	Assertion	hoadddi	$⊢ (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		simpl1	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \in ℂ$
2		ffvelcdm	$⊢ (T : ℋ ⟶ ℋ \land x \in ℋ) \to T (x) \in ℋ$
3	2	3ad2antl2	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to T (x) \in ℋ$
4		ffvelcdm	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to U (x) \in ℋ$
5	4	3ad2antl3	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to U (x) \in ℋ$
6		ax-hvdistr1	$⊢ (A \in ℂ \land T (x) \in ℋ \land U (x) \in ℋ) \to A \cdot_{ℎ} (T (x) +_{ℎ} U (x)) = (A \cdot_{ℎ} T (x)) +_{ℎ} (A \cdot_{ℎ} U (x))$
7	1 3 5 6	syl3anc	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T (x) +_{ℎ} U (x)) = (A \cdot_{ℎ} T (x)) +_{ℎ} (A \cdot_{ℎ} U (x))$
8		hosval	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to (T +_{op} U) (x) = T (x) +_{ℎ} U (x)$
9	8	oveq2d	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to A \cdot_{ℎ} (T +_{op} U) (x) = A \cdot_{ℎ} (T (x) +_{ℎ} U (x))$
10	9	3expa	$⊢ ((T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T +_{op} U) (x) = A \cdot_{ℎ} (T (x) +_{ℎ} U (x))$
11	10	3adantl1	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T +_{op} U) (x) = A \cdot_{ℎ} (T (x) +_{ℎ} U (x))$
12		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
13	12	3expa	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
14	13	3adantl3	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) = A \cdot_{ℎ} T (x)$
15		homval	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} U) (x) = A \cdot_{ℎ} U (x)$
16	15	3expa	$⊢ ((A \in ℂ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} U) (x) = A \cdot_{ℎ} U (x)$
17	16	3adantl2	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} U) (x) = A \cdot_{ℎ} U (x)$
18	14 17	oveq12d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (x) +_{ℎ} (A \cdot_{op} U) (x) = (A \cdot_{ℎ} T (x)) +_{ℎ} (A \cdot_{ℎ} U (x))$
19	7 11 18	3eqtr4d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T +_{op} U) (x) = (A \cdot_{op} T) (x) +_{ℎ} (A \cdot_{op} U) (x)$
20		hoaddcl	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T +_{op} U) : ℋ ⟶ ℋ$
21	20	anim2i	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (A \in ℂ \land (T +_{op} U) : ℋ ⟶ ℋ)$
22	21	3impb	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \in ℂ \land (T +_{op} U) : ℋ ⟶ ℋ)$
23		homval	$⊢ (A \in ℂ \land (T +_{op} U) : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} (T +_{op} U)) (x) = A \cdot_{ℎ} (T +_{op} U) (x)$
24	23	3expa	$⊢ ((A \in ℂ \land (T +_{op} U) : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T +_{op} U)) (x) = A \cdot_{ℎ} (T +_{op} U) (x)$
25	22 24	sylan	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T +_{op} U)) (x) = A \cdot_{ℎ} (T +_{op} U) (x)$
26		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
27		homulcl	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} U) : ℋ ⟶ ℋ$
28	26 27	anim12i	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (A \in ℂ \land U : ℋ ⟶ ℋ)) \to ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ)$
29	28	3impdi	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ)$
30		hosval	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (A \cdot_{op} U) (x)$
31	30	3expa	$⊢ (((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (A \cdot_{op} U) (x)$
32	29 31	sylan	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x) = (A \cdot_{op} T) (x) +_{ℎ} (A \cdot_{op} U) (x)$
33	19 25 32	3eqtr4d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T +_{op} U)) (x) = ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x)$
34	33	ralrimiva	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to \forall x \in ℋ (A \cdot_{op} (T +_{op} U)) (x) = ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x)$
35		homulcl	$⊢ (A \in ℂ \land (T +_{op} U) : ℋ ⟶ ℋ) \to (A \cdot_{op} (T +_{op} U)) : ℋ ⟶ ℋ$
36	20 35	sylan2	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (A \cdot_{op} (T +_{op} U)) : ℋ ⟶ ℋ$
37	36	3impb	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} (T +_{op} U)) : ℋ ⟶ ℋ$
38		hoaddcl	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) : ℋ ⟶ ℋ$
39	26 27 38	syl2an	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (A \in ℂ \land U : ℋ ⟶ ℋ)) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) : ℋ ⟶ ℋ$
40	39	3impdi	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) : ℋ ⟶ ℋ$
41		hoeq	$⊢ ((A \cdot_{op} (T +_{op} U)) : ℋ ⟶ ℋ \land ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) : ℋ ⟶ ℋ) \to (\forall x \in ℋ (A \cdot_{op} (T +_{op} U)) (x) = ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x) \leftrightarrow A \cdot_{op} (T +_{op} U) = (A \cdot_{op} T) +_{op} (A \cdot_{op} U))$
42	37 40 41	syl2anc	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (\forall x \in ℋ (A \cdot_{op} (T +_{op} U)) (x) = ((A \cdot_{op} T) +_{op} (A \cdot_{op} U)) (x) \leftrightarrow A \cdot_{op} (T +_{op} U) = (A \cdot_{op} T) +_{op} (A \cdot_{op} U))$
43	34 42	mpbid	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to A \cdot_{op} (T +_{op} U) = (A \cdot_{op} T) +_{op} (A \cdot_{op} U)$

Metamath Proof Explorer

Theorem hoadddi

Proof