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 ) ) )