Theorem hiassdi

Description: Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	hiassdi	|- ( ( ( A e. CC /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A .h B ) +h C ) .ih D ) = ( ( A x. ( B .ih D ) ) + ( C .ih D ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvmulcl	|- ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
2		ax-his2	|- ( ( ( A .h B ) e. ~H /\ C e. ~H /\ D e. ~H ) -> ( ( ( A .h B ) +h C ) .ih D ) = ( ( ( A .h B ) .ih D ) + ( C .ih D ) ) )
3	2	3expb	|- ( ( ( A .h B ) e. ~H /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A .h B ) +h C ) .ih D ) = ( ( ( A .h B ) .ih D ) + ( C .ih D ) ) )
4	1 3	sylan	|- ( ( ( A e. CC /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A .h B ) +h C ) .ih D ) = ( ( ( A .h B ) .ih D ) + ( C .ih D ) ) )
5		ax-his3	|- ( ( A e. CC /\ B e. ~H /\ D e. ~H ) -> ( ( A .h B ) .ih D ) = ( A x. ( B .ih D ) ) )
6	5	3expa	|- ( ( ( A e. CC /\ B e. ~H ) /\ D e. ~H ) -> ( ( A .h B ) .ih D ) = ( A x. ( B .ih D ) ) )
7	6	adantrl	|- ( ( ( A e. CC /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( A .h B ) .ih D ) = ( A x. ( B .ih D ) ) )
8	7	oveq1d	|- ( ( ( A e. CC /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A .h B ) .ih D ) + ( C .ih D ) ) = ( ( A x. ( B .ih D ) ) + ( C .ih D ) ) )
9	4 8	eqtrd	|- ( ( ( A e. CC /\ B e. ~H ) /\ ( C e. ~H /\ D e. ~H ) ) -> ( ( ( A .h B ) +h C ) .ih D ) = ( ( A x. ( B .ih D ) ) + ( C .ih D ) ) )