# Metamath Proof Explorer

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

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

### Proof

Step Hyp Ref Expression
1 ax-his2 ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}=\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
2 1 3comr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}=\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
3 hvaddcl ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{+}_{ℎ}{C}\in ℋ$
4 braval ${⊢}\left({A}\in ℋ\wedge {B}{+}_{ℎ}{C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{+}_{ℎ}{C}\right)=\left({B}{+}_{ℎ}{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}{+}_{ℎ}{C}\right)=\left({B}{+}_{ℎ}{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}{+}_{ℎ}{C}\right)=\left({B}{+}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}$
7 braval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)={B}{\cdot }_{\mathrm{ih}}{A}$
8 7 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)={B}{\cdot }_{\mathrm{ih}}{A}$
9 braval ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({C}\right)={C}{\cdot }_{\mathrm{ih}}{A}$
10 9 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}$
11 8 10 oveq12d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}\right)+\mathrm{bra}\left({A}\right)\left({C}\right)=\left({B}{\cdot }_{\mathrm{ih}}{A}\right)+\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
12 2 6 11 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \mathrm{bra}\left({A}\right)\left({B}{+}_{ℎ}{C}\right)=\mathrm{bra}\left({A}\right)\left({B}\right)+\mathrm{bra}\left({A}\right)\left({C}\right)$