# Metamath Proof Explorer

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

### Proof

Step Hyp Ref Expression
1 fvco3 ${⊢}\left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)$
2 1 3ad2antl3 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)$
3 fvco3 ${⊢}\left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to \left({T}\circ {U}\right)\left({x}\right)={T}\left({U}\left({x}\right)\right)$
4 3 3ad2antl3 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({T}\circ {U}\right)\left({x}\right)={T}\left({U}\left({x}\right)\right)$
5 4 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\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)$
6 ffvelrn ${⊢}\left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\to {U}\left({x}\right)\in ℋ$
7 homval ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}\left({x}\right)\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)={A}{\cdot }_{ℎ}{T}\left({U}\left({x}\right)\right)$
8 6 7 syl3an3 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge \left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)={A}{\cdot }_{ℎ}{T}\left({U}\left({x}\right)\right)$
9 8 3expa ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\wedge \left({U}:ℋ⟶ℋ\wedge {x}\in ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)={A}{\cdot }_{ℎ}{T}\left({U}\left({x}\right)\right)$
10 9 exp43 ${⊢}{A}\in ℂ\to \left({T}:ℋ⟶ℋ\to \left({U}:ℋ⟶ℋ\to \left({x}\in ℋ\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)={A}{\cdot }_{ℎ}{T}\left({U}\left({x}\right)\right)\right)\right)\right)$
11 10 3imp1 ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)={A}{\cdot }_{ℎ}{T}\left({U}\left({x}\right)\right)$
12 5 11 eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to {A}{\cdot }_{ℎ}\left({T}\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}{T}\right)\left({U}\left({x}\right)\right)$
13 2 12 eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\circ {U}\right)\left({x}\right)$
14 fco ${⊢}\left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({T}\circ {U}\right):ℋ⟶ℋ$
15 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)$
16 14 15 syl3an2 ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\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)$
17 16 3expia ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({x}\in ℋ\to \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\circ {U}\right)\left({x}\right)\right)$
18 17 3impb ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({x}\in ℋ\to \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)={A}{\cdot }_{ℎ}\left({T}\circ {U}\right)\left({x}\right)\right)$
19 18 imp ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\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)$
20 13 19 eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\wedge {x}\in ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)$
21 20 ralrimiva ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)$
22 homulcl ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ$
23 fco ${⊢}\left(\left({A}{·}_{\mathrm{op}}{T}\right):ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right):ℋ⟶ℋ$
24 22 23 stoic3 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right):ℋ⟶ℋ$
25 homulcl ${⊢}\left({A}\in ℂ\wedge \left({T}\circ {U}\right):ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right):ℋ⟶ℋ$
26 14 25 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\right)\to \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right):ℋ⟶ℋ$
27 26 3impb ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right):ℋ⟶ℋ$
28 hoeq ${⊢}\left(\left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right):ℋ⟶ℋ\wedge \left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right):ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)↔\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}={A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)$
29 24 27 28 syl2anc ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left(\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\left(\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}\right)\left({x}\right)=\left({A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)\left({x}\right)↔\left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}={A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)\right)$
30 21 29 mpbid ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\wedge {U}:ℋ⟶ℋ\right)\to \left({A}{·}_{\mathrm{op}}{T}\right)\circ {U}={A}{·}_{\mathrm{op}}\left({T}\circ {U}\right)$