# Metamath Proof Explorer

## Theorem homul12

Description: Swap first and second factors in a nested operator scalar product. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 mulcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}={B}{A}$
2 1 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}{·}_{\mathrm{op}}{T}={B}{A}{·}_{\mathrm{op}}{T}$
3 2 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{B}{·}_{\mathrm{op}}{T}={B}{A}{·}_{\mathrm{op}}{T}$
4 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)$
5 homulass ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {B}{A}{·}_{\mathrm{op}}{T}={B}{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
6 5 3com12 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {B}{A}{·}_{\mathrm{op}}{T}={B}{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
7 3 4 6 3eqtr3d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}\left({B}{·}_{\mathrm{op}}{T}\right)={B}{·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$