HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem distrlem5pr 5103
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)) (_ (A .P. (B +P. C)))
Proof of Theorem distrlem5pr
StepHypRef Expression
1 df-plp 5060 . . . . . . 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 1804 . . . . . . 7 |- w e. V
31, 2genpelv 5075 . . . . . 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 5094 . . . . . 6 |- ((A e. P. /\ B e. P.) -> (A .P. B) e. P.)
5 mulclpr 5094 . . . . . 6 |- ((A e. P. /\ C e. P.) -> (A .P. C) e. P.)
63, 4, 5syl2an 454 . . . . 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 5061 . . . . . . . . . . . 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 1804 . . . . . . . . . . . 12 |- v e. V
97, 8genpelv 5075 . . . . . . . . . . 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 5061 . . . . . . . . . . . 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 1804 . . . . . . . . . . . 12 |- u e. V
1210, 11genpelv 5075 . . . . . . . . . . 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))))
139, 12bi2anan9 630 . . . . . . . . . 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 1320 . . . . . . . . . 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))))
1513, 14syl6bbr 536 . . . . . . . . 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)))))
1615anbi1d 615 . . . . . . . 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 1301 . . . . . . . . . 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)))
18172exbii 1048 . . . . . . . . 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 1301 . . . . . . . . 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)))
2018, 19bitr 173 . . . . . . . 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)))
2116, 20syl6bbr 536 . . . . . . 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))))
22212exbidv 1276 . . . . . 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 1096 . . . . . . 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 1096 . . . . . . . . 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 1305 . . . . . . . . . . 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 439 . . . . . . . . . . . . 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 505 . . . . . . . . . . . . . . . 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)))
2827anbi1i 480 . . . . . . . . . . . . . . 15 |- ((((x e. A /\ f e. A) /\ (y e. B /\ z e. C)) /\ (v = (x .Q y) /\ u = (f .Q