homco2

Description: Move a scalar product out of a composition of operators. The operator T must be linear, unlike homco1 that works for any operators. (Contributed by NM, 13-Aug-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \in ℂ$
2		simpl3	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to U : ℋ ⟶ ℋ$
3		simpr	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to x \in ℋ$
4		homval	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} U) (x) = A \cdot_{ℎ} U (x)$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} U) (x) = A \cdot_{ℎ} U (x)$
6	5	fveq2d	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to T ((A \cdot_{op} U) (x)) = T (A \cdot_{ℎ} U (x))$
7		homulcl	$⊢ (A \in ℂ \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} U) : ℋ ⟶ ℋ$
8	7	3adant2	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} U) : ℋ ⟶ ℋ$
9		fvco3	$⊢ ((A \cdot_{op} U) : ℋ ⟶ ℋ \land x \in ℋ) \to (T \circ (A \cdot_{op} U)) (x) = T ((A \cdot_{op} U) (x))$
10	8 9	sylan	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T \circ (A \cdot_{op} U)) (x) = T ((A \cdot_{op} U) (x))$
11		fvco3	$⊢ (U : ℋ ⟶ ℋ \land x \in ℋ) \to (T \circ U) (x) = T (U (x))$
12	2 3 11	syl2anc	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T \circ U) (x) = T (U (x))$
13	12	oveq2d	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to A \cdot_{ℎ} (T \circ U) (x) = A \cdot_{ℎ} T (U (x))$
14		lnopf	$⊢ T \in LinOp \to T : ℋ ⟶ ℋ$
15	14	3ad2ant2	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to T : ℋ ⟶ ℋ$
16		simp3	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to U : ℋ ⟶ ℋ$
17		fco	$⊢ (T : ℋ ⟶ ℋ \land U : ℋ ⟶ ℋ) \to (T \circ U) : ℋ ⟶ ℋ$
18	15 16 17	syl2anc	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to (T \circ U) : ℋ ⟶ ℋ$
19	18	adantr	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T \circ U) : ℋ ⟶ ℋ$
20		homval	$⊢ (A \in ℂ \land (T \circ U) : ℋ ⟶ ℋ \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x)$
21	1 19 3 20	syl3anc	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = A \cdot_{ℎ} (T \circ U) (x)$
22		simpl2	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to T \in LinOp$
23	16	ffvelrnda	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to U (x) \in ℋ$
24		lnopmul	$⊢ (T \in LinOp \land A \in ℂ \land U (x) \in ℋ) \to T (A \cdot_{ℎ} U (x)) = A \cdot_{ℎ} T (U (x))$
25	22 1 23 24	syl3anc	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to T (A \cdot_{ℎ} U (x)) = A \cdot_{ℎ} T (U (x))$
26	13 21 25	3eqtr4d	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (A \cdot_{op} (T \circ U)) (x) = T (A \cdot_{ℎ} U (x))$
27	6 10 26	3eqtr4d	$⊢ ((A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \land x \in ℋ) \to (T \circ (A \cdot_{op} U)) (x) = (A \cdot_{op} (T \circ U)) (x)$
28	27	ralrimiva	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to \forall x \in ℋ (T \circ (A \cdot_{op} U)) (x) = (A \cdot_{op} (T \circ U)) (x)$
29		fco	$⊢ (T : ℋ ⟶ ℋ \land (A \cdot_{op} U) : ℋ ⟶ ℋ) \to (T \circ (A \cdot_{op} U)) : ℋ ⟶ ℋ$
30	15 8 29	syl2anc	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to (T \circ (A \cdot_{op} U)) : ℋ ⟶ ℋ$
31		simp1	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to A \in ℂ$
32		homulcl	$⊢ (A \in ℂ \land (T \circ U) : ℋ ⟶ ℋ) \to (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ$
33	31 18 32	syl2anc	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ$
34		hoeq	$⊢ ((T \circ (A \cdot_{op} U)) : ℋ ⟶ ℋ \land (A \cdot_{op} (T \circ U)) : ℋ ⟶ ℋ) \to (\forall x \in ℋ (T \circ (A \cdot_{op} U)) (x) = (A \cdot_{op} (T \circ U)) (x) \leftrightarrow T \circ (A \cdot_{op} U) = A \cdot_{op} (T \circ U))$
35	30 33 34	syl2anc	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to (\forall x \in ℋ (T \circ (A \cdot_{op} U)) (x) = (A \cdot_{op} (T \circ U)) (x) \leftrightarrow T \circ (A \cdot_{op} U) = A \cdot_{op} (T \circ U))$
36	28 35	mpbid	$⊢ (A \in ℂ \land T \in LinOp \land U : ℋ ⟶ ℋ) \to T \circ (A \cdot_{op} U) = A \cdot_{op} (T \circ U)$

Metamath Proof Explorer

Theorem homco2

Proof