Metamath Proof Explorer


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