# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in ℂ\wedge {T}\in \mathrm{LinOp}\wedge {U}:ℋ⟶ℋ\right)\to {T}\circ \left({A}{·}_{\mathrm{op}}{U}\right)={A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)$

### Proof

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