Theorem distrlem5pr 6283

Description: Lemma for distributive law for positive reals.

Assertion

Ref	Expression
distrlem5pr	|- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((A .P. B) +P. (A .P. C)) C_ (A .P. (B +P. C)))

Proof of Theorem distrlem5pr

Step	Hyp	Ref	Expression
1		df-plp 6240	. . . . . . 7 |- +P. = {<.<.x, y>., z>. | ((x e. P. /\ y e. P.) /\ z = {f | E.g e. x E.h e. y f = (g +Q h)})}
2		visset 2295	. . . . . . 7 |- w e. _V
3	1, 2	genpelv 6255	. . . . . 6 |- (((A .P. B) e. P. /\ (A .P. C) e. P.) -> (w e. ((A .P. B) +P. (A .P. C)) <-> E.vE.u((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u))))
4		mulclpr 6274	. . . . . 6 |- ((A e. P. /\ B e. P.) -> (A .P. B) e. P.)
5		mulclpr 6274	. . . . . 6 |- ((A e. P. /\ C e. P.) -> (A .P. C) e. P.)
6	3, 4, 5	syl2an 503	. . . . 5 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (w e. ((A .P. B) +P. (A .P. C)) <-> E.vE.u((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u))))
7		df-mp 6241	. . . . . . . . . . . 12 |- .P. = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {f | E.g e. w E.h e. v f = (g .Q h)})}
8		visset 2295	. . . . . . . . . . . 12 |- v e. _V
9	7, 8	genpelv 6255	. . . . . . . . . . 11 |- ((A e. P. /\ B e. P.) -> (v e. (A .P. B) <-> E.xE.y((x e. A /\ y e. B) /\ v = (x .Q y))))
10		df-mp 6241	. . . . . . . . . . . 12 |- .P. = {<.<.w, v>., u>. | ((w e. P. /\ v e. P.) /\ u = {x | E.g e. w E.h e. v x = (g .Q h)})}
11		visset 2295	. . . . . . . . . . . 12 |- u e. _V
12	10, 11	genpelv 6255	. . . . . . . . . . 11 |- ((A e. P. /\ C e. P.) -> (u e. (A .P. C) <-> E.fE.z((f e. A /\ z e. C) /\ u = (f .Q z))))
13	9, 12	bi2anan9 694	. . . . . . . . . 10 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> ((v e. (A .P. B) /\ u e. (A .P. C)) <-> (E.xE.y((x e. A /\ y e. B) /\ v = (x .Q y)) /\ E.fE.z((f e. A /\ z e. C) /\ u = (f .Q z)))))
14		ee4anv 1710	. . . . . . . . . 10 |- (E.xE.yE.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) <-> (E.xE.y((x e. A /\ y e. B) /\ v = (x .Q y)) /\ E.fE.z((f e. A /\ z e. C) /\ u = (f .Q z))))
15	13, 14	syl6bbr 597	. . . . . . . . 9 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> ((v e. (A .P. B) /\ u e. (A .P. C)) <-> E.xE.yE.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z)))))
16	15	anbi1d 679	. . . . . . . 8 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u)) <-> (E.xE.yE.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u))))
17		19.41vv 1686	. . . . . . . . . 10 |- (E.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> (E.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
18	17	2exbii 1399	. . . . . . . . 9 |- (E.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.xE.y(E.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
19		19.41vv 1686	. . . . . . . . 9 |- (E.xE.y(E.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> (E.xE.yE.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
20	18, 19	bitri 190	. . . . . . . 8 |- (E.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> (E.xE.yE.fE.z(((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
21	16, 20	syl6bbr 597	. . . . . . 7 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u)) <-> E.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u))))
22	21	2exbidv 1659	. . . . . 6 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (E.vE.u((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u)) <-> E.vE.uE.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u))))
23		exrot4 1454	. . . . . . 7 |- (E.vE.uE.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.xE.yE.vE.uE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
24		exrot4 1454	. . . . . . . . 9 |- (E.vE.uE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.fE.zE.vE.u((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
25		19.42vv 1690	. . . . . . . . . . 11 |- (E.vE.u(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ ((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))) <-> (((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ E.vE.u((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))))
26		anass 487	. . . . . . . . . . . . 13 |- (((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> (((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ ((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))))
27		an4 564	. . . . . . . . . . . . . . . 16 |- (((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) <-> ((x e. A /\ y e. B) /\ (f e. A /\ z e. C)))
28	27	anbi1i 539	. . . . . . . . . . . . . . 15 |- ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))) <-> (((x e. A /\ y e. B) /\ (f e. A /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))))
29		an4 564	. . . . . . . . . . . . . . 15 |- ((((x e. A /\ y e. B) /\ (f e. A /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))) <-> (((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))))
30	28, 29	bitri 190	. . . . . . . . . . . . . 14 |- ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))) <-> (((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))))
31	30	anbi1i 539	. . . . . . . . . . . . 13 |- (((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> ((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
32	26, 31	bitr3i 192	. . . . . . . . . . . 12 |- ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ ((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))) <-> ((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
33	32	2exbii 1399	. . . . . . . . . . 11 |- (E.vE.u(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ ((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))) <-> E.vE.u((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)))
34		oprex 4907	. . . . . . . . . . . . 13 |- (x .Q y) e. _V
35		oprex 4907	. . . . . . . . . . . . 13 |- (f .Q z) e. _V
36		id 73	. . . . . . . . . . . . . 14 |- ((v = (x .Q y) /\ u = (f .Q z)) -> (v = (x .Q y) /\ u = (f .Q z)))
37		opreq12 4891	. . . . . . . . . . . . . . 15 |- ((v = (x .Q y) /\ u = (f .Q z)) -> (v +Q u) = ((x .Q y) +Q (f .Q z)))
38	37	eqeq2d 1895	. . . . . . . . . . . . . 14 |- ((v = (x .Q y) /\ u = (f .Q z)) -> (w = (v +Q u) <-> w = ((x .Q y) +Q (f .Q z))))
39	36, 38	cgsex2g 2322	. . . . . . . . . . . . 13 |- (((x .Q y) e. _V /\ (f .Q z) e. _V) -> (E.vE.u((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u)) <-> w = ((x .Q y) +Q (f .Q z))))
40	34, 35, 39	mp2an 761	. . . . . . . . . . . 12 |- (E.vE.u((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u)) <-> w = ((x .Q y) +Q (f .Q z)))
41	40	anbi2i 538	. . . . . . . . . . 11 |- ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ E.vE.u((v = (x .Q y) /\ u = (f .Q z)) /\ w = (v +Q u))) <-> (((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
42	25, 33, 41	3bitr3i 198	. . . . . . . . . 10 |- (E.vE.u((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> (((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
43	42	2exbii 1399	. . . . . . . . 9 |- (E.fE.zE.vE.u((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
44	24, 43	bitri 190	. . . . . . . 8 |- (E.vE.uE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
45	44	2exbii 1399	. . . . . . 7 |- (E.xE.yE.vE.uE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
46	23, 45	bitri 190	. . . . . 6 |- (E.vE.uE.xE.yE.fE.z((((x e. A /\ y e. B) /\ v = (x .Q y)) /\ ((f e. A /\ z e. C) /\ u = (f .Q z))) /\ w = (v +Q u)) <-> E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))))
47	22, 46	syl6bb 595	. . . . 5 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (E.vE.u((v e. (A .P. B) /\ u e. (A .P. C)) /\ w = (v +Q u)) <-> E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z)))))
48	6, 47	bitrd 587	. . . 4 |- (((A e. P. /\ B e. P.) /\ (A e. P. /\ C e. P.)) -> (w e. ((A .P. B) +P. (A .P. C)) <-> E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z)))))
49	48	anandis 570	. . 3 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (w e. ((A .P. B) +P. (A .P. C)) <-> E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z)))))
50		eleq1 1957	. . . . . . 7 |- (w = ((x .Q y) +Q (f .Q z)) -> (w e. (A .P. (B +P. C)) <-> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C))))
51		distrlem4pr 6282	. . . . . . 7 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ ((x e. A /\ f e. A) /\ (y e. B /\ z e. C))) -> ((x .Q y) +Q (f .Q z)) e. (A .P. (B +P. C)))
52	50, 51	syl5cbir 228	. . . . . 6 |- (((A e. P. /\ (B e. P. /\ C e. P.)) /\ ((x e. A /\ f e. A) /\ (y e. B /\ z e. C))) -> (w = ((x .Q y) +Q (f .Q z)) -> w e. (A .P. (B +P. C))))
53	52	expimpd 404	. . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))) -> w e. (A .P. (B +P. C))))
54	53	19.23advv 1676	. . . 4 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (E.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))) -> w e. (A .P. (B +P. C))))
55	54	19.23advv 1676	. . 3 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (E.xE.yE.fE.z(((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ w = ((x .Q y) +Q (f .Q z))) -> w e. (A .P. (B +P. C))))
56	49, 55	sylbid 220	. 2 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (w e. ((A .P. B) +P. (A .P. C)) -> w e. (A .P. (B +P. C))))
57	56	ssrdv 2622	1 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> ((A .P. B) +P. (A .P. C)) C_ (A .P. (B +P. C)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292   C_ wss 2593  (class class class)co 4884   +Q cplq 6133   .Q cmq 6134  P.cnp 6137   +P. cpp 6139   .P. cmp 6140

This theorem is referenced by:  distrpr 6284

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-plp 6240  df-mp 6241

Copyright terms: Public domain