Metamath Proof Explorer


Theorem his35

Description: Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

Ref Expression
Assertion his35
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( ( A x. ( * ` B ) ) x. ( C .ih D ) ) )

Proof

Step Hyp Ref Expression
1 his5
 |-  ( ( B e. CC /\ C e. ~H /\ D e. ~H ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) )
2 1 3expb
 |-  ( ( B e. CC /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) )
3 2 adantll
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih ( B .h D ) ) = ( ( * ` B ) x. ( C .ih D ) ) )
4 3 oveq2d
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( A x. ( C .ih ( B .h D ) ) ) = ( A x. ( ( * ` B ) x. ( C .ih D ) ) ) )
5 simpll
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> A e. CC )
6 simprl
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> C e. ~H )
7 hvmulcl
 |-  ( ( B e. CC /\ D e. ~H ) -> ( B .h D ) e. ~H )
8 7 ad2ant2l
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( B .h D ) e. ~H )
9 ax-his3
 |-  ( ( A e. CC /\ C e. ~H /\ ( B .h D ) e. ~H ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( A x. ( C .ih ( B .h D ) ) ) )
10 5 6 8 9 syl3anc
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( A x. ( C .ih ( B .h D ) ) ) )
11 cjcl
 |-  ( B e. CC -> ( * ` B ) e. CC )
12 11 ad2antlr
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( * ` B ) e. CC )
13 hicl
 |-  ( ( C e. ~H /\ D e. ~H ) -> ( C .ih D ) e. CC )
14 13 adantl
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( C .ih D ) e. CC )
15 5 12 14 mulassd
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A x. ( * ` B ) ) x. ( C .ih D ) ) = ( A x. ( ( * ` B ) x. ( C .ih D ) ) ) )
16 4 10 15 3eqtr4d
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h C ) .ih ( B .h D ) ) = ( ( A x. ( * ` B ) ) x. ( C .ih D ) ) )