This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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