# Metamath Proof Explorer

## Theorem bramul

Description: Linearity property of bra for multiplication. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion bramul ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{\cdot }_{ℎ}{C}\right)={B}\mathrm{bra}\left({A}\right)\left({C}\right)$

### Proof

Step Hyp Ref Expression
1 ax-his3 ${⊢}\left({B}\in ℂ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \left({B}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}={B}\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
2 1 3comr ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \left({B}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}={B}\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
3 hvmulcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{ℎ}{C}\in ℋ$
4 braval ${⊢}\left({A}\in ℋ\wedge {B}{\cdot }_{ℎ}{C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{\cdot }_{ℎ}{C}\right)=\left({B}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}$
5 3 4 sylan2 ${⊢}\left({A}\in ℋ\wedge \left({B}\in ℂ\wedge {C}\in ℋ\right)\right)\to \mathrm{bra}\left({A}\right)\left({B}{\cdot }_{ℎ}{C}\right)=\left({B}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}$
6 5 3impb ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{\cdot }_{ℎ}{C}\right)=\left({B}{\cdot }_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}$
7 braval ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({C}\right)={C}{\cdot }_{\mathrm{ih}}{A}$
8 7 3adant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({C}\right)={C}{\cdot }_{\mathrm{ih}}{A}$
9 8 oveq2d ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to {B}\mathrm{bra}\left({A}\right)\left({C}\right)={B}\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
10 2 6 9 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℂ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{\cdot }_{ℎ}{C}\right)={B}\mathrm{bra}\left({A}\right)\left({C}\right)$