# Metamath Proof Explorer

## Theorem homulass

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

Ref Expression
Assertion homulass ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{B}{·}_{\mathrm{op}}{T}={A}{·}_{\mathrm{op}}\left({B}{·}_{\mathrm{op}}{T}\right)$

### Proof

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