# Metamath Proof Explorer

## Theorem brafnmul

Description: Anti-linearity property of bra functional for multiplication. (Contributed by NM, 31-May-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion brafnmul ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}{·}_{\mathrm{fn}}\mathrm{bra}\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 hvmulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{B}\in ℋ$
2 brafval ${⊢}{A}{\cdot }_{ℎ}{B}\in ℋ\to \mathrm{bra}\left({A}{\cdot }_{ℎ}{B}\right)=\left({x}\in ℋ⟼{x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
3 1 2 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}{\cdot }_{ℎ}{B}\right)=\left({x}\in ℋ⟼{x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
4 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
5 brafn ${⊢}{B}\in ℋ\to \mathrm{bra}\left({B}\right):ℋ⟶ℂ$
6 hfmmval ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge \mathrm{bra}\left({B}\right):ℋ⟶ℂ\right)\to \stackrel{‾}{{A}}{·}_{\mathrm{fn}}\mathrm{bra}\left({B}\right)=\left({x}\in ℋ⟼\stackrel{‾}{{A}}\mathrm{bra}\left({B}\right)\left({x}\right)\right)$
7 4 5 6 syl2an ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \stackrel{‾}{{A}}{·}_{\mathrm{fn}}\mathrm{bra}\left({B}\right)=\left({x}\in ℋ⟼\stackrel{‾}{{A}}\mathrm{bra}\left({B}\right)\left({x}\right)\right)$
8 his5 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\wedge {B}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{B}\right)$
9 8 3expa ${⊢}\left(\left({A}\in ℂ\wedge {x}\in ℋ\right)\wedge {B}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{B}\right)$
10 9 an32s ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{B}\right)$
11 braval ${⊢}\left({B}\in ℋ\wedge {x}\in ℋ\right)\to \mathrm{bra}\left({B}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{B}$
12 11 adantll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to \mathrm{bra}\left({B}\right)\left({x}\right)={x}{\cdot }_{\mathrm{ih}}{B}$
13 12 oveq2d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to \stackrel{‾}{{A}}\mathrm{bra}\left({B}\right)\left({x}\right)=\stackrel{‾}{{A}}\left({x}{\cdot }_{\mathrm{ih}}{B}\right)$
14 10 13 eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}\mathrm{bra}\left({B}\right)\left({x}\right)$
15 14 mpteq2dva ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({x}\in ℋ⟼{x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)\right)=\left({x}\in ℋ⟼\stackrel{‾}{{A}}\mathrm{bra}\left({B}\right)\left({x}\right)\right)$
16 7 15 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \stackrel{‾}{{A}}{·}_{\mathrm{fn}}\mathrm{bra}\left({B}\right)=\left({x}\in ℋ⟼{x}{\cdot }_{\mathrm{ih}}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
17 3 16 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \mathrm{bra}\left({A}{\cdot }_{ℎ}{B}\right)=\stackrel{‾}{{A}}{·}_{\mathrm{fn}}\mathrm{bra}\left({B}\right)$