Metamath Proof Explorer


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