homco1

Description: Associative law for scalar product and composition of operators. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fvco3	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} T) (U (x))$
2	1	3ad2antl3	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} T) (U (x))$
3		fvco3	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to (T \circ U) (x) = T (U (x))$
4	3	3ad2antl3	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T \circ U) (x) = T (U (x))$
5	4	oveq2d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T \circ U) (x) = A \cdot_{ℎ} T (U (x))$
6		ffvelcdm	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to U (x) \in ℋ$
7		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U (x) \in ℋ) \to (A \cdot_{op} T) (U (x)) = A \cdot_{ℎ} T (U (x))$
8	6 7	syl3an3	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land (U : ℋ ⟶ ℋ \land x \in ℋ)) \to (A \cdot_{op} T) (U (x)) = A \cdot_{ℎ} T (U (x))$
9	8	3expa	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ) \land (U : ℋ ⟶ ℋ \land x \in ℋ)) \to (A \cdot_{op} T) (U (x)) = A \cdot_{ℎ} T (U (x))$
10	9	exp43	$⊢ A \in ℂ \to (T : ℋ ⟶ ℋ \to (U : ℋ ⟶ ℋ \to (x \in ℋ \to (A \cdot_{op} T) (U (x)) = A \cdot_{ℎ} T (U (x)))))$
11	10	3imp1	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} T) (U (x)) = A \cdot_{ℎ} T (U (x))$
12	5 11	eqtr4d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T \circ U) (x) = (A \cdot_{op} T) (U (x))$
13	2 12	eqtr4d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) \circ U) (x) = A \cdot_{ℎ} (T \circ U) (x)$
14		fco	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T \circ U) : ℋ ⟶ ℋ$
15		homval	$⊢ (A \in ℂ \land (T \circ U) : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x)$
16	14 15	syl3an2	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x)$
17	16	3expia	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (x \in ℋ \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x))$
18	17	3impb	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (x \in ℋ \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x))$
19	18	imp	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x)$
20	13 19	eqtr4d	$⊢ ((A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} (T \circ U)) (x)$
21	20	ralrimiva	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to \forall x \in ℋ ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} (T \circ U)) (x)$
22		homulcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ) \to (A \cdot_{op} T) : ℋ ⟶ ℋ$
23		fco	$⊢ ((A \cdot_{op} T) : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) \circ U) : ℋ ⟶ ℋ$
24	22 23	stoic3	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to ((A \cdot_{op} T) \circ U) : ℋ ⟶ ℋ$
25		homulcl	$⊢ (A \in ℂ \land (T \circ U) : ℋ ⟶ ℋ) \to (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ$
26	14 25	sylan2	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ)) \to (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ$
27	26	3impb	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ$
28		hoeq	$⊢ (((A \cdot_{op} T) \circ U) : ℋ ⟶ ℋ \land (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ) \to (\forall x \in ℋ ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} (T \circ U)) (x) \leftrightarrow (A \cdot_{op} T) \circ U = A \cdot_{op} (T \circ U))$
29	24 27 28	syl2anc	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (\forall x \in ℋ ((A \cdot_{op} T) \circ U) (x) = (A \cdot_{op} (T \circ U)) (x) \leftrightarrow (A \cdot_{op} T) \circ U = A \cdot_{op} (T \circ U))$
30	21 29	mpbid	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} T) \circ U = A \cdot_{op} (T \circ U)$

Metamath Proof Explorer

Theorem homco1

Proof