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 
|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) ketbra C ) = ( B ketbra ( ( * ` A ) .h C ) ) )

Proof

Step Hyp Ref Expression
1 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
2 kbfval 
 |-  ( ( ( A .h B ) e. ~H /\ C e. ~H ) -> ( ( A .h B ) ketbra C ) = ( x e. ~H |-> ( ( x .ih C ) .h ( A .h B ) ) ) )
3 1 2 stoic3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) ketbra C ) = ( x e. ~H |-> ( ( x .ih C ) .h ( A .h B ) ) ) )
4 simp2 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> B e. ~H )
5 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
6 5 3ad2ant1 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( * ` A ) e. CC )
7 simp3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> C e. ~H )
8 hvmulcl 
 |-  ( ( ( * ` A ) e. CC /\ C e. ~H ) -> ( ( * ` A ) .h C ) e. ~H )
9 6 7 8 syl2anc 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( * ` A ) .h C ) e. ~H )
10 kbfval 
 |-  ( ( B e. ~H /\ ( ( * ` A ) .h C ) e. ~H ) -> ( B ketbra ( ( * ` A ) .h C ) ) = ( x e. ~H |-> ( ( x .ih ( ( * ` A ) .h C ) ) .h B ) ) )
11 4 9 10 syl2anc 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B ketbra ( ( * ` A ) .h C ) ) = ( x e. ~H |-> ( ( x .ih ( ( * ` A ) .h C ) ) .h B ) ) )
12 simpr 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> x e. ~H )
13 simpl3 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> C e. ~H )
14 hicl 
 |-  ( ( x e. ~H /\ C e. ~H ) -> ( x .ih C ) e. CC )
15 12 13 14 syl2anc 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( x .ih C ) e. CC )
16 simpl1 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> A e. CC )
17 simpl2 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> B e. ~H )
18 ax-hvmulass 
 |-  ( ( ( x .ih C ) e. CC /\ A e. CC /\ B e. ~H ) -> ( ( ( x .ih C ) x. A ) .h B ) = ( ( x .ih C ) .h ( A .h B ) ) )
19 15 16 17 18 syl3anc 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( x .ih C ) x. A ) .h B ) = ( ( x .ih C ) .h ( A .h B ) ) )
20 15 16 mulcomd 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( x .ih C ) x. A ) = ( A x. ( x .ih C ) ) )
21 his52 
 |-  ( ( A e. CC /\ x e. ~H /\ C e. ~H ) -> ( x .ih ( ( * ` A ) .h C ) ) = ( A x. ( x .ih C ) ) )
22 16 12 13 21 syl3anc 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( x .ih ( ( * ` A ) .h C ) ) = ( A x. ( x .ih C ) ) )
23 20 22 eqtr4d 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( x .ih C ) x. A ) = ( x .ih ( ( * ` A ) .h C ) ) )
24 23 oveq1d 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( ( x .ih C ) x. A ) .h B ) = ( ( x .ih ( ( * ` A ) .h C ) ) .h B ) )
25 19 24 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. ~H /\ C e. ~H ) /\ x e. ~H ) -> ( ( x .ih C ) .h ( A .h B ) ) = ( ( x .ih ( ( * ` A ) .h C ) ) .h B ) )
26 25 mpteq2dva 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( x e. ~H |-> ( ( x .ih C ) .h ( A .h B ) ) ) = ( x e. ~H |-> ( ( x .ih ( ( * ` A ) .h C ) ) .h B ) ) )
27 11 26 eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( B ketbra ( ( * ` A ) .h C ) ) = ( x e. ~H |-> ( ( x .ih C ) .h ( A .h B ) ) ) )
28 3 27 eqtr4d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) ketbra C ) = ( B ketbra ( ( * ` A ) .h C ) ) )