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