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	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A\left(B+C\right)=AB+AC$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cc	$$classℂ$$
2	0 1	wcel	$$wffA\in ℂ$$
3		cB	$$classB$$
4	3 1	wcel	$$wffB\in ℂ$$
5		cC	$$classC$$
6	5 1	wcel	$$wffC\in ℂ$$
7	2 4 6	w3a	$$wff\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)$$
8		cmul	$$class\times$$
9		caddc	$$class+$$
10	3 5 9	co	$$class\left(B+C\right)$$
11	0 10 8	co	$$classA\left(B+C\right)$$
12	0 3 8	co	$$classAB$$
13	0 5 8	co	$$classAC$$
14	12 13 9	co	$$class\left(AB+AC\right)$$
15	11 14	wceq	$$wffA\left(B+C\right)=AB+AC$$
16	7 15	wi	$$wff\left(\left(A\in ℂ\wedge B\in ℂ\wedge C\in ℂ\right)\to A\left(B+C\right)=AB+AC\right)$$