Theorem axdistr 9536

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 9560 be used later. Instead, use adddi 9582. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)

Assertion

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

Proof of Theorem axdistr

Dummy variables x y z w v u f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcnqs 9520	. 2 |- CC = ( ( R. X. R. ) /. `' _E )
2		addcnsrec 9521	. 2 |- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. z , w >. ] `' _E + [ <. v , u >. ] `' _E ) = [ <. ( z +R v ) , ( w +R u ) >. ] `' _E )
3		mulcnsrec 9522	. 2 |- ( ( ( x e. R. /\ y e. R. ) /\ ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. ( z +R v ) , ( w +R u ) >. ] `' _E ) = [ <. ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) , ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) >. ] `' _E )
4		mulcnsrec 9522	. 2 |- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. z , w >. ] `' _E ) = [ <. ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) , ( ( y .R z ) +R ( x .R w ) ) >. ] `' _E )
5		mulcnsrec 9522	. 2 |- ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. v , u >. ] `' _E ) = [ <. ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) , ( ( y .R v ) +R ( x .R u ) ) >. ] `' _E )
6		addcnsrec 9521	. 2 |- ( ( ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. /\ ( ( y .R z ) +R ( x .R w ) ) e. R. ) /\ ( ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. /\ ( ( y .R v ) +R ( x .R u ) ) e. R. ) ) -> ( [ <. ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) , ( ( y .R z ) +R ( x .R w ) ) >. ] `' _E + [ <. ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) , ( ( y .R v ) +R ( x .R u ) ) >. ] `' _E ) = [ <. ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) ) , ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) ) >. ] `' _E )
7		addclsr 9461	. . . 4 |- ( ( z e. R. /\ v e. R. ) -> ( z +R v ) e. R. )
8		addclsr 9461	. . . 4 |- ( ( w e. R. /\ u e. R. ) -> ( w +R u ) e. R. )
9	7, 8	anim12i 566	. . 3 |- ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
10	9	an4s 824	. 2 |- ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
11		mulclsr 9462	. . . . 5 |- ( ( x e. R. /\ z e. R. ) -> ( x .R z ) e. R. )
12		m1r 9460	. . . . . 6 |- -1R e. R.
13		mulclsr 9462	. . . . . 6 |- ( ( y e. R. /\ w e. R. ) -> ( y .R w ) e. R. )
14		mulclsr 9462	. . . . . 6 |- ( ( -1R e. R. /\ ( y .R w ) e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
15	12, 13, 14	sylancr 663	. . . . 5 |- ( ( y e. R. /\ w e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
16		addclsr 9461	. . . . 5 |- ( ( ( x .R z ) e. R. /\ ( -1R .R ( y .R w ) ) e. R. ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
17	11, 15, 16	syl2an 477	. . . 4 |- ( ( ( x e. R. /\ z e. R. ) /\ ( y e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
18	17	an4s 824	. . 3 |- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
19		mulclsr 9462	. . . . 5 |- ( ( y e. R. /\ z e. R. ) -> ( y .R z ) e. R. )
20		mulclsr 9462	. . . . 5 |- ( ( x e. R. /\ w e. R. ) -> ( x .R w ) e. R. )
21		addclsr 9461	. . . . 5 |- ( ( ( y .R z ) e. R. /\ ( x .R w ) e. R. ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
22	19, 20, 21	syl2anr 478	. . . 4 |- ( ( ( x e. R. /\ w e. R. ) /\ ( y e. R. /\ z e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
23	22	an42s 825	. . 3 |- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
24	18, 23	jca 532	. 2 |- ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. /\ ( ( y .R z ) +R ( x .R w ) ) e. R. ) )
25		mulclsr 9462	. . . . 5 |- ( ( x e. R. /\ v e. R. ) -> ( x .R v ) e. R. )
26		mulclsr 9462	. . . . . 6 |- ( ( y e. R. /\ u e. R. ) -> ( y .R u ) e. R. )
27		mulclsr 9462	. . . . . 6 |- ( ( -1R e. R. /\ ( y .R u ) e. R. ) -> ( -1R .R ( y .R u ) ) e. R. )
28	12, 26, 27	sylancr 663	. . . . 5 |- ( ( y e. R. /\ u e. R. ) -> ( -1R .R ( y .R u ) ) e. R. )
29		addclsr 9461	. . . . 5 |- ( ( ( x .R v ) e. R. /\ ( -1R .R ( y .R u ) ) e. R. ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
30	25, 28, 29	syl2an 477	. . . 4 |- ( ( ( x e. R. /\ v e. R. ) /\ ( y e. R. /\ u e. R. ) ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
31	30	an4s 824	. . 3 |- ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. )
32		mulclsr 9462	. . . . 5 |- ( ( y e. R. /\ v e. R. ) -> ( y .R v ) e. R. )
33		mulclsr 9462	. . . . 5 |- ( ( x e. R. /\ u e. R. ) -> ( x .R u ) e. R. )
34		addclsr 9461	. . . . 5 |- ( ( ( y .R v ) e. R. /\ ( x .R u ) e. R. ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
35	32, 33, 34	syl2anr 478	. . . 4 |- ( ( ( x e. R. /\ u e. R. ) /\ ( y e. R. /\ v e. R. ) ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
36	35	an42s 825	. . 3 |- ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( y .R v ) +R ( x .R u ) ) e. R. )
37	31, 36	jca 532	. 2 |- ( ( ( x e. R. /\ y e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) e. R. /\ ( ( y .R v ) +R ( x .R u ) ) e. R. ) )
38		distrsr 9469	. . . 4 |- ( x .R ( z +R v ) ) = ( ( x .R z ) +R ( x .R v ) )
39		distrsr 9469	. . . . . 6 |- ( y .R ( w +R u ) ) = ( ( y .R w ) +R ( y .R u ) )
40	39	oveq2i 6296	. . . . 5 |- ( -1R .R ( y .R ( w +R u ) ) ) = ( -1R .R ( ( y .R w ) +R ( y .R u ) ) )
41		distrsr 9469	. . . . 5 |- ( -1R .R ( ( y .R w ) +R ( y .R u ) ) ) = ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) )
42	40, 41	eqtri 2496	. . . 4 |- ( -1R .R ( y .R ( w +R u ) ) ) = ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) )
43	38, 42	oveq12i 6297	. . 3 |- ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) = ( ( ( x .R z ) +R ( x .R v ) ) +R ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) ) )
44		ovex 6310	. . . 4 |- ( x .R z ) e. _V
45		ovex 6310	. . . 4 |- ( x .R v ) e. _V
46		ovex 6310	. . . 4 |- ( -1R .R ( y .R w ) ) e. _V
47		addcomsr 9465	. . . 4 |- ( f +R g ) = ( g +R f )
48		addasssr 9466	. . . 4 |- ( ( f +R g ) +R h ) = ( f +R ( g +R h ) )
49		ovex 6310	. . . 4 |- ( -1R .R ( y .R u ) ) e. _V
50	44, 45, 46, 47, 48, 49	caov4 6491	. . 3 |- ( ( ( x .R z ) +R ( x .R v ) ) +R ( ( -1R .R ( y .R w ) ) +R ( -1R .R ( y .R u ) ) ) ) = ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) )
51	43, 50	eqtri 2496	. 2 |- ( ( x .R ( z +R v ) ) +R ( -1R .R ( y .R ( w +R u ) ) ) ) = ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) +R ( ( x .R v ) +R ( -1R .R ( y .R u ) ) ) )
52		distrsr 9469	. . . 4 |- ( y .R ( z +R v ) ) = ( ( y .R z ) +R ( y .R v ) )
53		distrsr 9469	. . . 4 |- ( x .R ( w +R u ) ) = ( ( x .R w ) +R ( x .R u ) )
54	52, 53	oveq12i 6297	. . 3 |- ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) = ( ( ( y .R z ) +R ( y .R v ) ) +R ( ( x .R w ) +R ( x .R u ) ) )
55		ovex 6310	. . . 4 |- ( y .R z ) e. _V
56		ovex 6310	. . . 4 |- ( y .R v ) e. _V
57		ovex 6310	. . . 4 |- ( x .R w ) e. _V
58		ovex 6310	. . . 4 |- ( x .R u ) e. _V
59	55, 56, 57, 47, 48, 58	caov4 6491	. . 3 |- ( ( ( y .R z ) +R ( y .R v ) ) +R ( ( x .R w ) +R ( x .R u ) ) ) = ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) )
60	54, 59	eqtri 2496	. 2 |- ( ( y .R ( z +R v ) ) +R ( x .R ( w +R u ) ) ) = ( ( ( y .R z ) +R ( x .R w ) ) +R ( ( y .R v ) +R ( x .R u ) ) )
61	1, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60	ecovdi 7420	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   _E cep 4789   `'ccnv 4998  (class class class)co 6285   R.cnr 9244   -1Rcm1r 9247   +R cplr 9248   .R cmr 9249   CCcc 9491   + caddc 9496   x. cmul 9498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-inf2 8059

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7043  df-rdg 7077  df-1o 7131  df-oadd 7135  df-omul 7136  df-er 7312  df-ec 7314  df-qs 7318  df-ni 9251  df-pli 9252  df-mi 9253  df-lti 9254  df-plpq 9287  df-mpq 9288  df-ltpq 9289  df-enq 9290  df-nq 9291  df-erq 9292  df-plq 9293  df-mq 9294  df-1nq 9295  df-rq 9296  df-ltnq 9297  df-np 9360  df-1p 9361  df-plp 9362  df-mp 9363  df-ltp 9364  df-enr 9434  df-nr 9435  df-plr 9436  df-mr 9437  df-m1r 9441  df-c 9499  df-add 9504  df-mul 9505

This theorem is referenced by: (None)