Theorem his35i

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

	Ref	Expression
Hypotheses	his35.1	|- A e. CC
	his35.2	|- B e. CC
	his35.3	|- C e. ~H
	his35.4	|- D e. ~H
Assertion	his35i	|- ( ( A .h C ) .ih ( B .h D ) ) = ( ( A x. ( * ` B ) ) x. ( C .ih D ) )

Proof

Step	Hyp	Ref	Expression
1		his35.1	|- A e. CC
2		his35.2	|- B e. CC
3		his35.3	|- C e. ~H
4		his35.4	|- D e. ~H
5		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 ) ) )
6	1 2 3 4 5	mp4an	|- ( ( A .h C ) .ih ( B .h D ) ) = ( ( A x. ( * ` B ) ) x. ( C .ih D ) )