HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem distrlem5pr 3925
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 3882 . . . . . . 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 1350 . . . . . . 7 |- w e. V
31, 2genpelv 3897 . . . . . 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 3916 . . . . . 6 |- ((A e. P. /\ B e. P.) -> (A .P B) e. P.)
5 mulclpr 3916 . . . . . 6 |- ((A e. P. /\ C e. P.) -> (A .P C) e. P.)
63, 4, 5syl2an 349 . . . . 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 3883 . . . . . . . . . . . 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 1350 . . . . . . . . . . . 12 |- v e. V
97, 8genpelv 3897 . . . . . . . . . . 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 3883 . . . . . . . . . . . 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 1350 . . . . . . . . . . . 12 |- u e. V
1210, 11genpelv 3897 . . . . . . . . . . 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 478 . . . . . . . . . 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 982 . . . . . . . . . 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 416 . . . . . . . . 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 469 . . . . . . . 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 964 . . . . . . . . . 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)))
1817bi2ex 734 . . . . . . . . 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 964 . . . . . . . . 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 151 . . . . . . . 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 416 . . . . . . 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))))
2221bi2exdv 938 . . . . . 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 778 . . . . . . 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 778 . . . . . . . . 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 968 . . . . . . . . . . 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 336 . . . . . . . . . . . . 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 388 . . . . . . . . . . . . . . . 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 368 . . . . . . . . . . . . . . 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) /\