Theorem adddir 10031

Description: Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)

Assertion

Ref	Expression
adddir	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )

Proof of Theorem adddir

Step	Hyp	Ref	Expression
1		adddi 10025	. . 3 |- ( ( C e. CC /\ A e. CC /\ B e. CC ) -> ( C x. ( A + B ) ) = ( ( C x. A ) + ( C x. B ) ) )
2	1	3coml 1272	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C x. ( A + B ) ) = ( ( C x. A ) + ( C x. B ) ) )
3		addcl 10018	. . 3 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4		mulcom 10022	. . 3 |- ( ( ( A + B ) e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( C x. ( A + B ) ) )
5	3, 4	stoic3 1701	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( C x. ( A + B ) ) )
6		mulcom 10022	. . . 4 |- ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
7	6	3adant2 1080	. . 3 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
8		mulcom 10022	. . . 4 |- ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
9	8	3adant1 1079	. . 3 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
10	7, 9	oveq12d 6668	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) + ( B x. C ) ) = ( ( C x. A ) + ( C x. B ) ) )
11	2, 5, 10	3eqtr4d 2666	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) x. C ) = ( ( A x. C ) + ( B x. C ) ) )

Syntax hints:   -> wi 4   /\ w3a 1037   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-addcl 9996  ax-mulcom 10000  ax-distr 10003

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  mulid1  10037  adddiri  10051  adddird  10065  muladd11  10206  00id  10211  cnegex2  10218  muladd  10462  ser1const  12857  hashxplem  13220  demoivreALT  14931  dvds2ln  15014  dvds2add  15015  odd2np1lem  15064  cncrng  19767  icccvx  22749  cnlmod  22940  sincosq1eq  24264  abssinper  24270  sineq0  24273  bposlem9  25017  cncvcOLD  27438  ipasslem1  27686  ipasslem11  27695  cdj3i  29300  mblfinlem3  33448  expgrowth  38534  fmtnofac2lem  41480  2zrngALT  41948