# Metamath Proof Explorer

## Theorem kbmul

Description: Multiplication property of outer product. (Contributed by NM, 31-May-2006) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hvmulcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{ℎ}{B}\in ℋ$
2 kbfval ${⊢}\left({A}{\cdot }_{ℎ}{B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right)\mathrm{ketbra}{C}=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
3 1 2 stoic3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right)\mathrm{ketbra}{C}=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
4 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}\in ℋ$
5 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
6 5 3ad2ant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}}\in ℂ$
7 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {C}\in ℋ$
8 hvmulcl ${⊢}\left(\stackrel{‾}{{A}}\in ℂ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\in ℋ$
9 6 7 8 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\in ℋ$
10 kbfval ${⊢}\left({B}\in ℋ\wedge \stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\in ℋ\right)\to {B}\mathrm{ketbra}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)\right){\cdot }_{ℎ}{B}\right)$
11 4 9 10 syl2anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}\mathrm{ketbra}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)\right){\cdot }_{ℎ}{B}\right)$
12 simpr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {x}\in ℋ$
13 simpl3 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {C}\in ℋ$
14 hicl ${⊢}\left({x}\in ℋ\wedge {C}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
15 12 13 14 syl2anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
16 simpl1 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {A}\in ℂ$
17 simpl2 ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {B}\in ℋ$
18 ax-hvmulass ${⊢}\left({x}{\cdot }_{\mathrm{ih}}{C}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){A}{\cdot }_{ℎ}{B}=\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)$
19 15 16 17 18 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){A}{\cdot }_{ℎ}{B}=\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)$
20 15 16 mulcomd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){A}={A}\left({x}{\cdot }_{\mathrm{ih}}{C}\right)$
21 his52 ${⊢}\left({A}\in ℂ\wedge {x}\in ℋ\wedge {C}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)={A}\left({x}{\cdot }_{\mathrm{ih}}{C}\right)$
22 16 12 13 21 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to {x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)={A}\left({x}{\cdot }_{\mathrm{ih}}{C}\right)$
23 20 22 eqtr4d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){A}={x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)$
24 23 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){A}{\cdot }_{ℎ}{B}=\left({x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)\right){\cdot }_{ℎ}{B}$
25 19 24 eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\wedge {x}\in ℋ\right)\to \left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\left({x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)\right){\cdot }_{ℎ}{B}$
26 25 mpteq2dva ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)\right){\cdot }_{ℎ}{B}\right)$
27 11 26 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}\mathrm{ketbra}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)=\left({x}\in ℋ⟼\left({x}{\cdot }_{\mathrm{ih}}{C}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)\right)$
28 3 27 eqtr4d ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}\right)\mathrm{ketbra}{C}={B}\mathrm{ketbra}\left(\stackrel{‾}{{A}}{\cdot }_{ℎ}{C}\right)$