Axiom ax-hvdistr1

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvdistr1	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cc	|- CC
2	0 1	wcel	|- A e. CC
3		cB	|- B
4		chba	|- ~H
5	3 4	wcel	|- B e. ~H
6		cC	|- C
7	6 4	wcel	|- C e. ~H
8	2 5 7	w3a	|- ( A e. CC /\ B e. ~H /\ C e. ~H )
9		csm	|- .h
10		cva	|- +h
11	3 6 10	co	|- ( B +h C )
12	0 11 9	co	|- ( A .h ( B +h C ) )
13	0 3 9	co	|- ( A .h B )
14	0 6 9	co	|- ( A .h C )
15	13 14 10	co	|- ( ( A .h B ) +h ( A .h C ) )
16	12 15	wceq	|- ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) )
17	8 16	wi	|- ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B +h C ) ) = ( ( A .h B ) +h ( A .h C ) ) )