Axiom ax-distr

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr . Proofs should normally use adddi instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

	Ref	Expression
Assertion	ax-distr	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. 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	3 1	wcel	|- B e. CC
5		cC	|- C
6	5 1	wcel	|- C e. CC
7	2 4 6	w3a	|- ( A e. CC /\ B e. CC /\ C e. CC )
8		cmul	|- x.
9		caddc	|- +
10	3 5 9	co	|- ( B + C )
11	0 10 8	co	|- ( A x. ( B + C ) )
12	0 3 8	co	|- ( A x. B )
13	0 5 8	co	|- ( A x. C )
14	12 13 9	co	|- ( ( A x. B ) + ( A x. C ) )
15	11 14	wceq	|- ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) )
16	7 15	wi	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )